Theorem 3expb 1147

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
3expb	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1145	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 254	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

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

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

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

This theorem is referenced by:  3adant3r1  1155  3adant3r2  1156  3adant3r3  1157  3adant1l  1173  3adant1r  1174  mp3an1  1267  soinxp  4537  sotri  4860  fnfco  5220  mpt2eq3dva  5751  fovrnda  5826  ovelrn  5831  grprinvd  5878  nnmsucr  6289  fidifsnid  6667  exmidpw  6704  undiffi  6715  fidcenumlemim  6741  ltpopr  7251  ltexprlemdisj  7262  recexprlemdisj  7286  mul4  7711  add4  7740  2addsub  7793  addsubeq4  7794  subadd4  7823  muladd  7959  ltleadd  8021  divmulap  8239  divap0  8248  div23ap  8255  div12ap  8258  divsubdirap  8272  divcanap5  8278  divmuleqap  8281  divcanap6  8283  divdiv32ap  8284  div2subap  8399  letrp1  8406  lemul12b  8419  lediv1  8427  cju  8519  nndivre  8556  nndivtr  8562  nn0addge1  8817  nn0addge2  8818  peano2uz2  8952  uzind  8956  uzind3  8958  fzind  8960  fnn0ind  8961  uzind4  9175  qre  9209  irrmul  9231  rpdivcl  9258  rerpdivcl  9263  iccshftr  9560  iccshftl  9562  iccdil  9564  icccntr  9566  fzaddel  9622  fzrev  9647  frec2uzf1od  9962  expdivap  10137  2shfti  10396  iooinsup  10836  isermulc2  10899  dvds2add  11273  dvds2sub  11274  dvdstr  11276  alzdvds  11298  divalg2  11369  lcmgcdlem  11502  lcmgcdeq  11508  isprm6  11569  tgclb  11933  topbas  11935  neissex  12033  cnpnei  12086  psmetxrge0  12134  psmetlecl  12136  xmetlecl  12169  xmettpos  12172  elbl3ps  12196  elbl3  12197  metss  12296  comet  12301  bdxmet  12303  bdmet  12304  bl2ioo  12332  cncffvrn  12351  divccncfap  12359