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  2777  po2nr  4822  fliftfund  6212  frfi  7783  fin33i  8766  axdc3lem4  8850  iscatd  15090  isfuncd  15281  isposd  15712  pospropd  15891  imasmnd2  16084  grpinveu  16211  grpid  16212  imasgrp2  16312  dmdprdd  17157  pgpfac1lem5  17257  imasring  17395  islmodd  17645  lmodvsghm  17698  islssd  17709  islmhm2  17811  psrbaglefi  18150  psrbaglefiOLD  18151  mulgghm2  18658  mulgghm2OLD  18661  isphld  18816  riinopn  19544  ordtbaslem  19816  subbascn  19882  haust1  19980  isnrm2  19986  isnrm3  19987  lmmo  20008  nllyidm  20116  tx1stc  20277  filin  20481  filtop  20482  isfil2  20483  infil  20490  fgfil  20502  isufil2  20535  ufileu  20546  filufint  20547  flimopn  20602  flimrest  20610  isxmetd  20955  met2ndc  21152  icccmplem2  21454  lmmbr  21823  cfil3i  21834  equivcfil  21864  bcthlem5  21893  volfiniun  22083  dvidlem  22445  ulmdvlem3  22923  ax5seg  24368  axcontlem4  24397  axcont  24406  grporcan  25350  grpoinveu  25351  grpoid  25352  grpoasscan1  25366  cvxpcon  28884  cvxscon  28885  mclsax  29126  mclsppslem  29140  relexpaddd  29279  predpo  29481  broutsideof2  29977  nn0prpwlem  30345  fgmin  30393  cntotbnd  30497  heiborlem6  30517  heiborlem10  30521  rngonegmn1l  30557  rngonegmn1r  30558  rngoneglmul  30559  rngonegrmul  30560  crngm23  30604  prnc  30669  pridlc3  30675  dmncan1  30678  lsmsat  34876  eqlkr  34967  llncmp  35389  2at0mat0  35392  llncvrlpln  35425  lplncmp  35429  lplnexllnN  35431  lplncvrlvol  35483  lvolcmp  35484  linepsubN  35619  pmapsub  35635  paddasslem16  35702  pmodlem2  35714  lhp2lt  35868  ltrneq2  36015  cdlemf2  36431  cdlemk34  36779  cdlemn11pre  37080  dihord2pre  37095