Theorem 3exp2 1214

Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3exp2.1	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )

Assertion

Ref	Expression
3exp2	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Proof of Theorem 3exp2

Step	Hyp	Ref	Expression
1		3exp2.1	. . 3 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
2	1	ex 434	. 2 |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
3	2	3expd 1213	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975

This theorem is referenced by:  3anassrs  1218  pm2.61da3ne  2787  po2nr  4813  fliftfund  6199  frfi  7765  fin33i  8749  axdc3lem4  8833  iscatd  14928  isfuncd  15092  isposd  15442  pospropd  15621  imasmnd2  15776  grpinveu  15894  grpid  15895  imasgrp2  15995  dmdprdd  16833  pgpfac1lem5  16932  imasrng  17069  islmodd  17318  lmodvsghm  17371  islssd  17382  islmhm2  17484  psrbaglefi  17822  psrbaglefiOLD  17823  mulgghm2  18326  mulgghm2OLD  18329  isphld  18484  riinopn  19212  ordtbaslem  19483  subbascn  19549  haust1  19647  isnrm2  19653  isnrm3  19654  lmmo  19675  nllyidm  19784  tx1stc  19914  filin  20118  filtop  20119  isfil2  20120  infil  20127  fgfil  20139  isufil2  20172  ufileu  20183  filufint  20184  flimopn  20239  flimrest  20247  isxmetd  20592  met2ndc  20789  icccmplem2  21091  lmmbr  21460  cfil3i  21471  equivcfil  21501  bcthlem5  21530  volfiniun  21720  dvidlem  22082  ulmdvlem3  22559  ax5seg  23945  axcontlem4  23974  axcont  23983  grporcan  24927  grpoinveu  24928  grpoid  24929  grpoasscan1  24943  cvxpcon  28355  cvxscon  28356  predpo  28869  broutsideof2  29377  nn0prpwlem  29745  fgmin  29819  cntotbnd  29923  heiborlem6  29943  heiborlem10  29947  rngonegmn1l  29983  rngonegmn1r  29984  rngoneglmul  29985  rngonegrmul  29986  crngm23  30030  prnc  30095  pridlc3  30101  dmncan1  30104  lsmsat  33823  eqlkr  33914  llncmp  34336  2at0mat0  34339  llncvrlpln  34372  lplncmp  34376  lplnexllnN  34378  lplncvrlvol  34430  lvolcmp  34431  linepsubN  34566  pmapsub  34582  paddasslem16  34649  pmodlem2  34661  lhp2lt  34815  ltrneq2  34962  cdlemf2  35376  cdlemk34  35724  cdlemn11pre  36025  dihord2pre  36040