Theorem 3expa 1138

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3anidm23  1228  mp3an2  1256  mpd3an3  1269  rgen3  2448  moi2  2773  sbc3ie  2887  preq12bg  3565  issod  4074  wepo  4114  reuhypd  4221  funimass4  5245  fvtp1g  5390  f1imass  5434  fcof1o  5449  f1ofveu  5520  f1ocnvfv3  5521  acexmid  5531  2ndrn  5829  rdgon  5996  frecrdg  6015  findcard  6372  findcard2  6373  findcard2s  6374  ltapig  6528  ltanqi  6592  ltmnqi  6593  lt2addnq  6594  lt2mulnq  6595  prarloclemcalc  6692  genpassl  6714  genpassu  6715  prmuloc  6756  ltexprlemm  6790  ltexprlemfl  6799  ltexprlemfu  6801  lteupri  6807  ltaprg  6809  mul4  7240  add4  7269  cnegexlem2  7284  cnegexlem3  7285  2addsub  7322  addsubeq4  7323  muladd  7488  ltleadd  7550  reapmul1  7695  apreim  7703  receuap  7759  p1le  7927  lemul12b  7939  lbinf  8026  zdiv  8435  fzind  8462  fnn0ind  8463  uzss  8639  qmulcl  8722  qreccl  8727  xrlttr  8870  icc0r  8949  iooshf  8975  elfz5  9037  elfz0fzfz0  9137  fzind2  9248  ioo0  9268  ico0  9270  ioc0  9271  expnegap0  9484  expineg2  9485  mulexpzap  9516  expsubap  9524  expnbnd  9596  facndiv  9666  bccmpl  9681  ibcval5  9690  bcpasc  9693  crim  9745  climshftlemg  10141  dvdsval3  10199  dvdsnegb  10212  muldvds1  10220  muldvds2  10221  dvdscmul  10222  dvdsmulc  10223  dvds2ln  10228  divalgb  10325  ndvdssub  10330  gcddiv  10408  rpexp1i  10533