Theorem 3exp2 1198

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

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

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 960

This theorem is referenced by:  3anassrs  1202  po2nr  4641  fliftfund  5993  frfi  7545  fin33i  8526  axdc3lem4  8610  iscatd  14594  isfuncd  14758  isposd  15108  pospropd  15287  imasmnd2  15441  grpinveu  15552  grpid  15553  imasgrp2  15650  dmdprdd  16455  pgpfac1lem5  16554  imasrng  16646  islmodd  16878  lmodvsghm  16930  islssd  16939  islmhm2  17041  psrbaglefi  17375  psrbaglefiOLD  17376  mulgghm2  17767  mulgghm2OLD  17770  isphld  17925  riinopn  18363  ordtbaslem  18634  subbascn  18700  haust1  18798  isnrm2  18804  isnrm3  18805  lmmo  18826  nllyidm  18935  tx1stc  19065  filin  19269  filtop  19270  isfil2  19271  infil  19278  fgfil  19290  isufil2  19323  ufileu  19334  filufint  19335  flimopn  19390  flimrest  19398  isxmetd  19743  met2ndc  19940  icccmplem2  20242  lmmbr  20611  cfil3i  20622  equivcfil  20652  bcthlem5  20681  volfiniun  20870  dvidlem  21232  ulmdvlem3  21752  ax5seg  23007  axcontlem4  23036  axcont  23045  grporcan  23531  grpoinveu  23532  grpoid  23533  grpoasscan1  23547  cvxpcon  26979  cvxscon  26980  predpo  27492  broutsideof2  28000  nn0prpwlem  28361  fgmin  28435  cntotbnd  28539  heiborlem6  28559  heiborlem10  28563  rngonegmn1l  28599  rngonegmn1r  28600  rngoneglmul  28601  rngonegrmul  28602  crngm23  28646  prnc  28711  pridlc3  28717  dmncan1  28720  lsmsat  32247  eqlkr  32338  llncmp  32760  2at0mat0  32763  llncvrlpln  32796  lplncmp  32800  lplnexllnN  32802  lplncvrlvol  32854  lvolcmp  32855  linepsubN  32990  pmapsub  33006  paddasslem16  33073  pmodlem2  33085  lhp2lt  33239  ltrneq2  33386  cdlemf2  33800  cdlemk34  34148  cdlemn11pre  34449  dihord2pre  34464