Theorem 3exp2 1205

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 1204	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

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

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 967

This theorem is referenced by:  3anassrs  1209  po2nr  4649  fliftfund  6001  frfi  7549  fin33i  8530  axdc3lem4  8614  iscatd  14603  isfuncd  14767  isposd  15117  pospropd  15296  imasmnd2  15450  grpinveu  15563  grpid  15564  imasgrp2  15661  dmdprdd  16469  pgpfac1lem5  16568  imasrng  16699  islmodd  16932  lmodvsghm  16984  islssd  16994  islmhm2  17096  psrbaglefi  17418  psrbaglefiOLD  17419  mulgghm2  17900  mulgghm2OLD  17903  isphld  18058  riinopn  18496  ordtbaslem  18767  subbascn  18833  haust1  18931  isnrm2  18937  isnrm3  18938  lmmo  18959  nllyidm  19068  tx1stc  19198  filin  19402  filtop  19403  isfil2  19404  infil  19411  fgfil  19423  isufil2  19456  ufileu  19467  filufint  19468  flimopn  19523  flimrest  19531  isxmetd  19876  met2ndc  20073  icccmplem2  20375  lmmbr  20744  cfil3i  20755  equivcfil  20785  bcthlem5  20814  volfiniun  21003  dvidlem  21365  ulmdvlem3  21842  ax5seg  23135  axcontlem4  23164  axcont  23173  grporcan  23659  grpoinveu  23660  grpoid  23661  grpoasscan1  23675  cvxpcon  27083  cvxscon  27084  predpo  27596  broutsideof2  28104  nn0prpwlem  28470  fgmin  28544  cntotbnd  28648  heiborlem6  28668  heiborlem10  28672  rngonegmn1l  28708  rngonegmn1r  28709  rngoneglmul  28710  rngonegrmul  28711  crngm23  28755  prnc  28820  pridlc3  28826  dmncan1  28829  lsmsat  32493  eqlkr  32584  llncmp  33006  2at0mat0  33009  llncvrlpln  33042  lplncmp  33046  lplnexllnN  33048  lplncvrlvol  33100  lvolcmp  33101  linepsubN  33236  pmapsub  33252  paddasslem16  33319  pmodlem2  33331  lhp2lt  33485  ltrneq2  33632  cdlemf2  34046  cdlemk34  34394  cdlemn11pre  34695  dihord2pre  34710