Theorem 3exp2 1206

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 1205	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  1210  pm2.61da3ne  2771  po2nr  4761  fliftfund  6114  frfi  7667  fin33i  8648  axdc3lem4  8732  iscatd  14729  isfuncd  14893  isposd  15243  pospropd  15422  imasmnd2  15576  grpinveu  15690  grpid  15691  imasgrp2  15788  dmdprdd  16602  pgpfac1lem5  16701  imasrng  16833  islmodd  17076  lmodvsghm  17128  islssd  17139  islmhm2  17241  psrbaglefi  17563  psrbaglefiOLD  17564  mulgghm2  18049  mulgghm2OLD  18052  isphld  18207  riinopn  18652  ordtbaslem  18923  subbascn  18989  haust1  19087  isnrm2  19093  isnrm3  19094  lmmo  19115  nllyidm  19224  tx1stc  19354  filin  19558  filtop  19559  isfil2  19560  infil  19567  fgfil  19579  isufil2  19612  ufileu  19623  filufint  19624  flimopn  19679  flimrest  19687  isxmetd  20032  met2ndc  20229  icccmplem2  20531  lmmbr  20900  cfil3i  20911  equivcfil  20941  bcthlem5  20970  volfiniun  21160  dvidlem  21522  ulmdvlem3  21999  ax5seg  23335  axcontlem4  23364  axcont  23373  grporcan  23859  grpoinveu  23860  grpoid  23861  grpoasscan1  23875  cvxpcon  27274  cvxscon  27275  predpo  27788  broutsideof2  28296  nn0prpwlem  28664  fgmin  28738  cntotbnd  28842  heiborlem6  28862  heiborlem10  28866  rngonegmn1l  28902  rngonegmn1r  28903  rngoneglmul  28904  rngonegrmul  28905  crngm23  28949  prnc  29014  pridlc3  29020  dmncan1  29023  lsmsat  32976  eqlkr  33067  llncmp  33489  2at0mat0  33492  llncvrlpln  33525  lplncmp  33529  lplnexllnN  33531  lplncvrlvol  33583  lvolcmp  33584  linepsubN  33719  pmapsub  33735  paddasslem16  33802  pmodlem2  33814  lhp2lt  33968  ltrneq2  34115  cdlemf2  34529  cdlemk34  34877  cdlemn11pre  35178  dihord2pre  35193