Theorem 3expb 1139

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 1137	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 253	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:  3adant3r1  1147  3adant3r2  1148  3adant3r3  1149  3adant1l  1161  3adant1r  1162  mp3an1  1255  soinxp  4428  sotri  4740  fnfco  5085  mpt2eq3dva  5589  fovrnda  5664  ovelrn  5669  grprinvd  5716  nnmsucr  6090  ltpopr  6785  ltexprlemdisj  6796  recexprlemdisj  6820  mul4  7240  add4  7269  2addsub  7322  addsubeq4  7323  subadd4  7352  muladd  7488  ltleadd  7550  divmulap  7763  divap0  7772  div23ap  7779  div12ap  7782  divsubdirap  7796  divcanap5  7802  divmuleqap  7805  divcanap6  7807  divdiv32ap  7808  letrp1  7926  lemul12b  7939  lediv1  7947  cju  8038  nndivre  8074  nndivtr  8080  nn0addge1  8334  nn0addge2  8335  peano2uz2  8454  uzind  8458  uzind3  8460  fzind  8462  fnn0ind  8463  uzind4  8676  qre  8710  irrmul  8732  rpdivcl  8759  rerpdivcl  8764  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  fzaddel  9077  fzrev  9101  frec2uzf1od  9408  expdivap  9527  2shfti  9719  iisermulc2  10178  dvds2add  10229  dvds2sub  10230  dvdstr  10232  alzdvds  10254  divalg2  10326  lcmgcdlem  10459  lcmgcdeq  10465  isprm6  10526