Theorem 3expa 1229

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 1228	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

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

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 1006

This theorem is referenced by:  ad4ant123  1241  ad4ant124  1242  ad4ant134  1243  ad4ant234  1244  ad5ant123  1265  3anidm23  1333  mp3an2  1361  mpd3an3  1374  rgen3  2619  moi2  2987  sbc3ie  3105  2if2dc  3645  preq12bg  3856  issod  4416  wepo  4456  reuhypd  4568  funimass4  5696  fvtp1g  5861  f1imass  5914  fcof1o  5929  f1ofveu  6005  f1ocnvfv3  6006  acexmid  6016  2ndrn  6345  frecrdg  6573  oawordriexmid  6637  mapxpen  7033  findcard  7076  findcard2  7077  findcard2s  7078  ltapig  7557  ltanqi  7621  ltmnqi  7622  lt2addnq  7623  lt2mulnq  7624  prarloclemcalc  7721  genpassl  7743  genpassu  7744  prmuloc  7785  ltexprlemm  7819  ltexprlemfl  7828  ltexprlemfu  7830  lteupri  7836  ltaprg  7838  mul4  8310  add4  8339  cnegexlem2  8354  cnegexlem3  8355  2addsub  8392  addsubeq4  8393  muladd  8562  ltleadd  8625  reapmul1  8774  apreim  8782  receuap  8848  p1le  9028  lemul12b  9040  lbinf  9127  zdiv  9567  fzind  9594  fnn0ind  9595  uzss  9776  qmulcl  9870  qreccl  9875  xrlttr  10029  xaddass  10103  icc0r  10160  iooshf  10186  elfz5  10251  elfz0fzfz0  10360  fzind2  10484  ioo0  10518  ico0  10520  ioc0  10521  expnegap0  10808  expineg2  10809  mulexpzap  10840  expsubap  10848  expnbnd  10924  facndiv  11000  bccmpl  11015  bcval5  11024  bcpasc  11027  ccatrn  11185  swrdspsleq  11247  swrdccat2  11251  ccatpfx  11281  pfxccat1  11282  swrdswrd  11285  cats1un  11301  crim  11418  climshftlemg  11862  2sumeq2dv  11931  hash2iun  12039  2cprodeq2dv  12128  dvdsval3  12351  dvdsnegb  12368  muldvds1  12376  muldvds2  12377  dvdscmul  12378  dvdsmulc  12379  dvds2ln  12384  divalgb  12485  ndvdssub  12490  gcddiv  12589  rpexp1i  12725  phiprmpw  12793  hashgcdeq  12811  pythagtriplem1  12837  pockthg  12929  infpnlem1  12931  4sqlem3  12962  imasaddfnlemg  13396  mndpfo  13520  grplmulf1o  13656  grplactcnv  13684  mulgnn0subcl  13721  mulgsubcl  13722  mulgdir  13740  issubg2m  13775  issubgrpd2  13776  nmzsubg  13796  eqgen  13813  ghmmulg  13842  ghmf1  13859  kerf1ghm  13860  conjghm  13862  srglmhm  14005  srgrmhm  14006  ringlghm  14073  ringrghm  14074  oppr1g  14094  dvdsrcl2  14112  crngunit  14124  subsubrng  14227  subrgugrp  14253  subsubrg  14258  islmod  14304  lmodvsdir  14325  lmodvsass  14326  lsssubg  14390  lss1d  14396  lidlsubg  14499  lidlsubcl  14500  expghmap  14620  mulgghm2  14621  innei  14886  iscnp4  14941  cnpnei  14942  cnnei  14955  cnconst  14957  ismeti  15069  isxmet2d  15071  elbl2ps  15115  elbl2  15116  xblpnfps  15121  xblpnf  15122  xblm  15140  blininf  15147  blssexps  15152  blssex  15153  blsscls2  15216  metss  15217  metrest  15229  metcn  15237  divcnap  15288  cdivcncfap  15327  dvply1  15488  lgslem4  15731  lgscllem  15735  lgsneg1  15753  lgsne0  15766  uspgr2wlkeq  16215