Theorem 3exp2 1223

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  3anassrs  1228  pm2.61da3ne  2744  po2nr  4783  predpo  5413  fliftfund  6217  frfi  7818  fin33i  8799  axdc3lem4  8883  relexpaddd  13105  iscatd  15566  isfuncd  15757  isposd  16188  pospropd  16367  imasmnd2  16560  grpinveu  16687  grpid  16688  imasgrp2  16788  dmdprdd  17618  pgpfac1lem5  17699  imasring  17834  islmodd  18084  lmodvsghm  18136  islssd  18146  islmhm2  18248  psrbaglefi  18583  mulgghm2  19054  isphld  19207  riinopn  19924  ordtbaslem  20190  subbascn  20256  haust1  20354  isnrm2  20360  isnrm3  20361  lmmo  20382  nllyidm  20490  tx1stc  20651  filin  20855  filtop  20856  isfil2  20857  infil  20864  fgfil  20876  isufil2  20909  ufileu  20920  filufint  20921  flimopn  20976  flimrest  20984  isxmetd  21327  met2ndc  21524  icccmplem2  21827  lmmbr  22214  cfil3i  22225  equivcfil  22255  bcthlem5  22282  volfiniun  22486  dvidlem  22856  ulmdvlem3  23343  ax5seg  24954  axcontlem4  24983  axcont  24992  grporcan  25934  grpoinveu  25935  grpoid  25936  grpoasscan1  25950  cvxpcon  29960  cvxscon  29961  mclsax  30202  mclsppslem  30216  broutsideof2  30881  nn0prpwlem  30970  fgmin  31018  poimirlem27  31880  poimirlem29  31882  poimirlem31  31884  cntotbnd  32041  heiborlem6  32061  heiborlem10  32065  rngonegmn1l  32101  rngonegmn1r  32102  rngoneglmul  32103  rngonegrmul  32104  crngm23  32148  prnc  32213  pridlc3  32219  dmncan1  32222  lsmsat  32492  eqlkr  32583  llncmp  33005  2at0mat0  33008  llncvrlpln  33041  lplncmp  33045  lplnexllnN  33047  lplncvrlvol  33099  lvolcmp  33100  linepsubN  33235  pmapsub  33251  paddasslem16  33318  pmodlem2  33330  lhp2lt  33484  ltrneq2  33631  cdlemf2  34047  cdlemk34  34395  cdlemn11pre  34696  dihord2pre  34711