Theorem 3expb 1207

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3adant3r1  1215  3adant3r2  1216  3adant3r3  1217  3adant1l  1233  3adant1r  1234  mp3an1  1337  soinxp  4746  sotri  5079  fnfco  5452  mpoeq3dva  6011  fovcdmda  6092  ovelrn  6097  fnmpoovd  6303  nnmsucr  6576  fidifsnid  6970  exmidpw  7007  undiffi  7024  fidcenumlemim  7056  ltpopr  7710  ltexprlemdisj  7721  recexprlemdisj  7745  mul4  8206  add4  8235  2addsub  8288  addsubeq4  8289  subadd4  8318  muladd  8458  ltleadd  8521  divmulap  8750  divap0  8759  div23ap  8766  div12ap  8769  divsubdirap  8783  divcanap5  8789  divmuleqap  8792  divcanap6  8794  divdiv32ap  8795  div2subap  8912  letrp1  8923  lemul12b  8936  lediv1  8944  cju  9036  nndivre  9074  nndivtr  9080  nn0addge1  9343  nn0addge2  9344  peano2uz2  9482  uzind  9486  uzind3  9488  fzind  9490  fnn0ind  9491  uzind4  9711  qre  9748  irrmul  9770  rpdivcl  9803  rerpdivcl  9808  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  fzaddel  10183  fzrev  10208  frec2uzf1od  10553  expdivap  10737  fundm2domnop0  10992  swrdwrdsymbg  11120  ccatpfx  11155  2shfti  11175  iooinsup  11621  isermulc2  11684  dvds2add  12169  dvds2sub  12170  dvdstr  12172  alzdvds  12198  divalg2  12270  lcmgcdlem  12432  lcmgcdeq  12438  isprm6  12502  pcqcl  12662  mgmplusf  13231  grpinva  13251  ismndd  13302  imasmnd2  13317  idmhm  13334  issubm2  13338  submid  13342  0mhm  13351  resmhm  13352  resmhm2  13353  resmhm2b  13354  mhmco  13355  mhmima  13356  gsumwsubmcl  13361  gsumwmhm  13363  grpinvcnv  13433  grpinvnzcl  13437  grpsubf  13444  imasgrp2  13479  qusgrp2  13482  mhmfmhm  13486  mulgnnsubcl  13503  mulgnn0z  13518  mulgnndir  13520  issubg4m  13562  isnsg3  13576  nsgid  13584  qusadd  13603  ghmmhm  13622  ghmmhmb  13623  idghm  13628  resghm  13629  ghmf1  13642  kerf1ghm  13643  qusghm  13651  ghmfghm  13695  invghm  13698  ablnsg  13703  srgfcl  13768  srgmulgass  13784  srglmhm  13788  srgrmhm  13789  ringlghm  13856  ringrghm  13857  opprringbg  13875  mulgass3  13880  isnzr2  13979  subrngringnsg  14000  issubrng2  14005  issubrg2  14036  domnmuln0  14068  islmodd  14088  lmodscaf  14105  lcomf  14122  rmodislmodlem  14145  issubrgd  14247  qusrhm  14323  qusmul2  14324  crngridl  14325  qusmulrng  14327  znidom  14452  psraddcl  14475  tgclb  14570  topbas  14572  neissex  14670  cnpnei  14724  txcnp  14776  psmetxrge0  14837  psmetlecl  14839  xmetlecl  14872  xmettpos  14875  elbl3ps  14899  elbl3  14900  metss  14999  comet  15004  bdxmet  15006  bdmet  15007  bl2ioo  15055  divcnap  15070  cncfcdm  15087  divccncfap  15095  dvrecap  15218  dvmptfsum  15230  cosz12  15285  gausslemma2dlem1a  15568