Theorem 3expa 1227

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

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

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 1004

This theorem is referenced by:  ad4ant123  1239  ad4ant124  1240  ad4ant134  1241  ad4ant234  1242  ad5ant123  1263  3anidm23  1331  mp3an2  1359  mpd3an3  1372  rgen3  2617  moi2  2984  sbc3ie  3102  2if2dc  3642  preq12bg  3851  issod  4410  wepo  4450  reuhypd  4562  funimass4  5684  fvtp1g  5847  f1imass  5898  fcof1o  5913  f1ofveu  5989  f1ocnvfv3  5990  acexmid  6000  2ndrn  6329  frecrdg  6554  oawordriexmid  6616  mapxpen  7009  findcard  7050  findcard2  7051  findcard2s  7052  ltapig  7525  ltanqi  7589  ltmnqi  7590  lt2addnq  7591  lt2mulnq  7592  prarloclemcalc  7689  genpassl  7711  genpassu  7712  prmuloc  7753  ltexprlemm  7787  ltexprlemfl  7796  ltexprlemfu  7798  lteupri  7804  ltaprg  7806  mul4  8278  add4  8307  cnegexlem2  8322  cnegexlem3  8323  2addsub  8360  addsubeq4  8361  muladd  8530  ltleadd  8593  reapmul1  8742  apreim  8750  receuap  8816  p1le  8996  lemul12b  9008  lbinf  9095  zdiv  9535  fzind  9562  fnn0ind  9563  uzss  9743  qmulcl  9832  qreccl  9837  xrlttr  9991  xaddass  10065  icc0r  10122  iooshf  10148  elfz5  10213  elfz0fzfz0  10322  fzind2  10445  ioo0  10479  ico0  10481  ioc0  10482  expnegap0  10769  expineg2  10770  mulexpzap  10801  expsubap  10809  expnbnd  10885  facndiv  10961  bccmpl  10976  bcval5  10985  bcpasc  10988  ccatrn  11144  swrdspsleq  11199  swrdccat2  11203  ccatpfx  11233  pfxccat1  11234  swrdswrd  11237  cats1un  11253  crim  11369  climshftlemg  11813  2sumeq2dv  11882  hash2iun  11990  2cprodeq2dv  12079  dvdsval3  12302  dvdsnegb  12319  muldvds1  12327  muldvds2  12328  dvdscmul  12329  dvdsmulc  12330  dvds2ln  12335  divalgb  12436  ndvdssub  12441  gcddiv  12540  rpexp1i  12676  phiprmpw  12744  hashgcdeq  12762  pythagtriplem1  12788  pockthg  12880  infpnlem1  12882  4sqlem3  12913  imasaddfnlemg  13347  mndpfo  13471  grplmulf1o  13607  grplactcnv  13635  mulgnn0subcl  13672  mulgsubcl  13673  mulgdir  13691  issubg2m  13726  issubgrpd2  13727  nmzsubg  13747  eqgen  13764  ghmmulg  13793  ghmf1  13810  kerf1ghm  13811  conjghm  13813  srglmhm  13956  srgrmhm  13957  ringlghm  14024  ringrghm  14025  oppr1g  14045  dvdsrcl2  14063  crngunit  14075  subsubrng  14178  subrgugrp  14204  subsubrg  14209  islmod  14255  lmodvsdir  14276  lmodvsass  14277  lsssubg  14341  lss1d  14347  lidlsubg  14450  lidlsubcl  14451  expghmap  14571  mulgghm2  14572  innei  14837  iscnp4  14892  cnpnei  14893  cnnei  14906  cnconst  14908  ismeti  15020  isxmet2d  15022  elbl2ps  15066  elbl2  15067  xblpnfps  15072  xblpnf  15073  xblm  15091  blininf  15098  blssexps  15103  blssex  15104  blsscls2  15167  metss  15168  metrest  15180  metcn  15188  divcnap  15239  cdivcncfap  15278  dvply1  15439  lgslem4  15682  lgscllem  15686  lgsneg1  15704  lgsne0  15717  uspgr2wlkeq  16076