Theorem 3expb 1144

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 1142	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 253	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

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

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 926

This theorem is referenced by:  3adant3r1  1152  3adant3r2  1153  3adant3r3  1154  3adant1l  1166  3adant1r  1167  mp3an1  1260  soinxp  4508  sotri  4827  fnfco  5185  mpt2eq3dva  5713  fovrnda  5788  ovelrn  5793  grprinvd  5840  nnmsucr  6249  fidifsnid  6587  exmidpw  6624  undiffi  6635  fidcenumlemim  6661  ltpopr  7154  ltexprlemdisj  7165  recexprlemdisj  7189  mul4  7614  add4  7643  2addsub  7696  addsubeq4  7697  subadd4  7726  muladd  7862  ltleadd  7924  divmulap  8142  divap0  8151  div23ap  8158  div12ap  8161  divsubdirap  8175  divcanap5  8181  divmuleqap  8184  divcanap6  8186  divdiv32ap  8187  div2subap  8302  letrp1  8309  lemul12b  8322  lediv1  8330  cju  8421  nndivre  8458  nndivtr  8464  nn0addge1  8719  nn0addge2  8720  peano2uz2  8853  uzind  8857  uzind3  8859  fzind  8861  fnn0ind  8862  uzind4  9076  qre  9110  irrmul  9132  rpdivcl  9159  rerpdivcl  9164  iccshftr  9411  iccshftl  9413  iccdil  9415  icccntr  9417  fzaddel  9473  fzrev  9498  frec2uzf1od  9813  expdivap  10006  2shfti  10265  iisermulc2  10728  dvds2add  11108  dvds2sub  11109  dvdstr  11111  alzdvds  11133  divalg2  11204  lcmgcdlem  11337  lcmgcdeq  11343  isprm6  11404  cncffvrn  11638  divccncfap  11646