Theorem 3expb 1204

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

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

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 980

This theorem is referenced by:  3adant3r1  1212  3adant3r2  1213  3adant3r3  1214  3adant1l  1230  3adant1r  1231  mp3an1  1324  soinxp  4698  sotri  5026  fnfco  5392  mpoeq3dva  5941  fovcdmda  6020  ovelrn  6025  fnmpoovd  6218  nnmsucr  6491  fidifsnid  6873  exmidpw  6910  undiffi  6926  fidcenumlemim  6953  ltpopr  7596  ltexprlemdisj  7607  recexprlemdisj  7631  mul4  8091  add4  8120  2addsub  8173  addsubeq4  8174  subadd4  8203  muladd  8343  ltleadd  8405  divmulap  8634  divap0  8643  div23ap  8650  div12ap  8653  divsubdirap  8667  divcanap5  8673  divmuleqap  8676  divcanap6  8678  divdiv32ap  8679  div2subap  8796  letrp1  8807  lemul12b  8820  lediv1  8828  cju  8920  nndivre  8957  nndivtr  8963  nn0addge1  9224  nn0addge2  9225  peano2uz2  9362  uzind  9366  uzind3  9368  fzind  9370  fnn0ind  9371  uzind4  9590  qre  9627  irrmul  9649  rpdivcl  9681  rerpdivcl  9686  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fzaddel  10061  fzrev  10086  frec2uzf1od  10408  expdivap  10573  2shfti  10842  iooinsup  11287  isermulc2  11350  dvds2add  11834  dvds2sub  11835  dvdstr  11837  alzdvds  11862  divalg2  11933  lcmgcdlem  12079  lcmgcdeq  12085  isprm6  12149  pcqcl  12308  mgmplusf  12790  grprinvd  12810  ismndd  12843  idmhm  12865  issubm2  12869  submid  12873  0mhm  12878  mhmco  12879  mhmima  12880  grpinvcnv  12943  grpinvnzcl  12947  grpsubf  12954  mhmfmhm  12986  mulgnnsubcl  13000  mulgnn0z  13015  mulgnndir  13017  issubg4m  13058  isnsg3  13072  nsgid  13080  srgfcl  13161  srgmulgass  13177  srglmhm  13181  srgrmhm  13182  opprringbg  13255  mulgass3  13259  issubrg2  13367  islmodd  13388  lmodscaf  13405  lcomf  13422  rmodislmodlem  13445  tgclb  13650  topbas  13652  neissex  13750  cnpnei  13804  txcnp  13856  psmetxrge0  13917  psmetlecl  13919  xmetlecl  13952  xmettpos  13955  elbl3ps  13979  elbl3  13980  metss  14079  comet  14084  bdxmet  14086  bdmet  14087  bl2ioo  14127  divcnap  14140  cncfcdm  14154  divccncfap  14162  dvrecap  14262  cosz12  14286