Theorem 3exp2 1285

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 450	. 2 |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
3	2	3expd 1284	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anassrs  1290  pm2.61da3ne  2883  po2nr  5048  predpo  5698  fliftfund  6563  frfi  8205  fin33i  9191  axdc3lem4  9275  relexpaddd  13794  iscatd  16334  isfuncd  16525  isposd  16955  pospropd  17134  imasmnd2  17327  grpinveu  17456  grpid  17457  grpasscan1  17478  imasgrp2  17530  dmdprdd  18398  pgpfac1lem5  18478  imasring  18619  islmodd  18869  lmodvsghm  18924  islssd  18936  islmhm2  19038  psrbaglefi  19372  mulgghm2  19845  isphld  19999  riinopn  20713  ordtbaslem  20992  subbascn  21058  haust1  21156  isnrm2  21162  isnrm3  21163  lmmo  21184  nllyidm  21292  tx1stc  21453  filin  21658  filtop  21659  isfil2  21660  infil  21667  fgfil  21679  isufil2  21712  ufileu  21723  filufint  21724  flimopn  21779  flimrest  21787  isxmetd  22131  met2ndc  22328  icccmplem2  22626  lmmbr  23056  cfil3i  23067  equivcfil  23097  bcthlem5  23125  volfiniun  23315  dvidlem  23679  ulmdvlem3  24156  ax5seg  25818  axcontlem4  25847  axcont  25856  grporcan  27372  grpoinveu  27373  grpoid  27374  cvxpconn  31224  cvxsconn  31225  mclsax  31466  mclsppslem  31480  broutsideof2  32229  nn0prpwlem  32317  fgmin  32365  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  cntotbnd  33595  heiborlem6  33615  heiborlem10  33619  rngonegmn1l  33740  rngonegmn1r  33741  rngoneglmul  33742  rngonegrmul  33743  crngm23  33801  prnc  33866  pridlc3  33872  dmncan1  33875  lsmsat  34295  eqlkr  34386  llncmp  34808  2at0mat0  34811  llncvrlpln  34844  lplncmp  34848  lplnexllnN  34850  lplncvrlvol  34902  lvolcmp  34903  linepsubN  35038  pmapsub  35054  paddasslem16  35121  pmodlem2  35133  lhp2lt  35287  ltrneq2  35434  cdlemf2  35850  cdlemk34  36198  cdlemn11pre  36499  dihord2pre  36514