Theorem 3expa 1182

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  ad4ant123  1194  ad4ant124  1195  ad4ant134  1196  ad4ant234  1197  3anidm23  1276  mp3an2  1304  mpd3an3  1317  rgen3  2522  moi2  2869  sbc3ie  2986  preq12bg  3708  issod  4249  wepo  4289  reuhypd  4400  funimass4  5480  fvtp1g  5636  f1imass  5683  fcof1o  5698  f1ofveu  5770  f1ocnvfv3  5771  acexmid  5781  2ndrn  6089  frecrdg  6313  oawordriexmid  6374  mapxpen  6750  findcard  6790  findcard2  6791  findcard2s  6792  ltapig  7170  ltanqi  7234  ltmnqi  7235  lt2addnq  7236  lt2mulnq  7237  prarloclemcalc  7334  genpassl  7356  genpassu  7357  prmuloc  7398  ltexprlemm  7432  ltexprlemfl  7441  ltexprlemfu  7443  lteupri  7449  ltaprg  7451  mul4  7918  add4  7947  cnegexlem2  7962  cnegexlem3  7963  2addsub  8000  addsubeq4  8001  muladd  8170  ltleadd  8232  reapmul1  8381  apreim  8389  receuap  8454  p1le  8631  lemul12b  8643  lbinf  8730  zdiv  9163  fzind  9190  fnn0ind  9191  uzss  9370  qmulcl  9456  qreccl  9461  xrlttr  9611  xaddass  9682  icc0r  9739  iooshf  9765  elfz5  9829  elfz0fzfz0  9934  fzind2  10047  ioo0  10068  ico0  10070  ioc0  10071  expnegap0  10332  expineg2  10333  mulexpzap  10364  expsubap  10372  expnbnd  10446  facndiv  10517  bccmpl  10532  bcval5  10541  bcpasc  10544  crim  10662  climshftlemg  11103  2sumeq2dv  11172  hash2iun  11280  2cprodeq2dv  11369  dvdsval3  11533  dvdsnegb  11546  muldvds1  11554  muldvds2  11555  dvdscmul  11556  dvdsmulc  11557  dvds2ln  11562  divalgb  11658  ndvdssub  11663  gcddiv  11743  rpexp1i  11868  phiprmpw  11934  hashgcdeq  11940  innei  12371  iscnp4  12426  cnpnei  12427  cnnei  12440  cnconst  12442  ismeti  12554  isxmet2d  12556  elbl2ps  12600  elbl2  12601  xblpnfps  12606  xblpnf  12607  xblm  12625  blininf  12632  blssexps  12637  blssex  12638  blsscls2  12701  metss  12702  metrest  12714  metcn  12722  divcnap  12763  cdivcncfap  12795