Theorem 3expa 1234

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3expa	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1233	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  ad4ant123  1246  ad4ant124  1247  ad4ant134  1248  ad4ant234  1249  ad5ant123  1270  3anidm23  1338  mp3an2  1366  mpd3an3  1379  rgen3  2637  moi2  3007  sbc3ie  3125  2if2dc  3677  preq12bg  3893  issod  4459  wepo  4499  reuhypd  4612  funimass4  5747  fvtp1g  5914  f1imass  5970  fcof1o  5985  f1ofveu  6063  f1ocnvfv3  6064  acexmid  6074  2ndrn  6407  funsssuppss  6488  frecrdg  6669  oawordriexmid  6733  mapxpen  7138  findcard  7182  findcard2  7183  findcard2s  7184  ltapig  7695  ltanqi  7759  ltmnqi  7760  lt2addnq  7761  lt2mulnq  7762  prarloclemcalc  7859  genpassl  7881  genpassu  7882  prmuloc  7923  ltexprlemm  7957  ltexprlemfl  7966  ltexprlemfu  7968  lteupri  7974  ltaprg  7976  mul4  8448  add4  8477  cnegexlem2  8492  cnegexlem3  8493  2addsub  8530  addsubeq4  8531  muladd  8701  ltleadd  8764  reapmul1  8913  apreim  8921  receuap  8989  p1le  9169  lemul12b  9181  lbinf  9268  zdiv  9713  fzind  9740  fnn0ind  9741  uzss  9922  qmulcl  10016  qreccl  10021  xrlttr  10176  xaddass  10250  icc0r  10307  iooshf  10333  elfz5  10399  elfz0fzfz0  10511  fzind2  10636  ioo0  10672  ico0  10674  ioc0  10675  expnegap0  10962  expineg2  10963  mulexpzap  10994  expsubap  11002  expnbnd  11079  facndiv  11155  bccmpl  11170  bcval5  11179  bcpasc  11182  ccatrn  11355  swrdspsleq  11417  swrdccat2  11421  ccatpfx  11451  pfxccat1  11452  swrdswrd  11455  cats1un  11471  crim  11601  climshftlemg  12046  2sumeq2dv  12115  hash2iun  12224  2cprodeq2dv  12313  dvdsval3  12536  dvdsnegb  12553  muldvds1  12561  muldvds2  12562  dvdscmul  12563  dvdsmulc  12564  dvds2ln  12569  divalgb  12670  ndvdssub  12675  gcddiv  12774  rpexp1i  12910  phiprmpw  12978  hashgcdeq  12996  pythagtriplem1  13022  pockthg  13114  infpnlem1  13116  4sqlem3  13147  imasaddfnlemg  13612  mndpfo  13728  grplmulf1o  13856  grplactcnv  13884  mulgnn0subcl  13915  mulgsubcl  13916  mulgdir  13934  issubg2m  13969  issubgrpd2  13970  nmzsubg  13990  eqgen  14007  ghmmulg  14036  ghmf1  14053  kerf1ghm  14054  conjghm  14056  srglmhm  14271  srgrmhm  14272  ringlghm  14339  ringrghm  14340  oppr1g  14361  dvdsrcl2  14379  crngunit  14391  subsubrng  14495  subrgugrp  14521  subsubrg  14526  islmod  14600  lmodvsdir  14621  lmodvsass  14622  lsssubg  14686  lss1d  14692  lidlsubg  14795  lidlsubcl  14796  expghmap  14914  mulgghm2  14915  innei  15187  iscnp4  15242  cnpnei  15243  cnnei  15256  cnconst  15258  ismeti  15370  isxmet2d  15372  elbl2ps  15416  elbl2  15417  xblpnfps  15422  xblpnf  15423  xblm  15441  blininf  15448  blssexps  15453  blssex  15454  blsscls2  15517  metss  15518  metrest  15530  metcn  15538  divcnap  15589  cdivcncfap  15628  dvply1  15789  lgslem4  16036  lgscllem  16040  lgsneg1  16058  lgsne0  16071  uspgr2wlkeq  16520  eupth2lem3lem7fi  16629