Theorem 3exp2 1171

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

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  3anassrs  1175  po2nr  4476  fliftfund  5994  frfi  7311  fin33i  8205  axdc3lem4  8289  iscatd  13853  isfuncd  14017  isposd  14367  joinle  14405  pospropd  14516  imasmnd2  14687  grpinveu  14794  grpid  14795  imasgrp2  14888  dmdprdd  15515  pgpfac1lem5  15592  imasrng  15680  islmodd  15911  lmodvsghm  15960  islssd  15967  islmhm2  16069  psrbaglefi  16392  mulgghm2  16741  isphld  16840  riinopn  16936  ordtbaslem  17206  subbascn  17272  haust1  17370  isnrm2  17376  isnrm3  17377  lmmo  17398  nllyidm  17505  tx1stc  17635  filin  17839  filtop  17840  isfil2  17841  infil  17848  fgfil  17860  isufil2  17893  ufileu  17904  filufint  17905  flimopn  17960  flimrest  17968  isxmetd  18309  met2ndc  18506  icccmplem2  18807  lmmbr  19164  cfil3i  19175  equivcfil  19205  bcthlem5  19234  volfiniun  19394  dvidlem  19755  ulmdvlem3  20271  grporcan  21762  grpoinveu  21763  grpoid  21764  grpoasscan1  21778  cvxpcon  24882  cvxscon  24883  predpo  25398  ax5seg  25781  axcontlem4  25810  axcont  25819  broutsideof2  25960  nn0prpwlem  26215  fgmin  26289  cntotbnd  26395  heiborlem6  26415  heiborlem10  26419  rngonegmn1l  26455  rngonegmn1r  26456  rngoneglmul  26457  rngonegrmul  26458  crngm23  26502  prnc  26567  pridlc3  26573  dmncan1  26576  lsmsat  29491  eqlkr  29582  llncmp  30004  2at0mat0  30007  llncvrlpln  30040  lplncmp  30044  lplnexllnN  30046  lplncvrlvol  30098  lvolcmp  30099  linepsubN  30234  pmapsub  30250  paddasslem16  30317  pmodlem2  30329  lhp2lt  30483  ltrneq2  30630  cdlemf2  31044  cdlemk34  31392  cdlemn11pre  31693  dihord2pre  31708

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938