Theorem 3expb 1206

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

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

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 982

This theorem is referenced by:  3adant3r1  1214  3adant3r2  1215  3adant3r3  1216  3adant1l  1232  3adant1r  1233  mp3an1  1335  soinxp  4717  sotri  5045  fnfco  5412  mpoeq3dva  5964  fovcdmda  6044  ovelrn  6049  fnmpoovd  6244  nnmsucr  6517  fidifsnid  6903  exmidpw  6940  undiffi  6957  fidcenumlemim  6985  ltpopr  7629  ltexprlemdisj  7640  recexprlemdisj  7664  mul4  8124  add4  8153  2addsub  8206  addsubeq4  8207  subadd4  8236  muladd  8376  ltleadd  8438  divmulap  8667  divap0  8676  div23ap  8683  div12ap  8686  divsubdirap  8700  divcanap5  8706  divmuleqap  8709  divcanap6  8711  divdiv32ap  8712  div2subap  8829  letrp1  8840  lemul12b  8853  lediv1  8861  cju  8953  nndivre  8990  nndivtr  8996  nn0addge1  9257  nn0addge2  9258  peano2uz2  9395  uzind  9399  uzind3  9401  fzind  9403  fnn0ind  9404  uzind4  9624  qre  9661  irrmul  9683  rpdivcl  9715  rerpdivcl  9720  iccshftr  10030  iccshftl  10032  iccdil  10034  icccntr  10036  fzaddel  10095  fzrev  10120  frec2uzf1od  10443  expdivap  10611  2shfti  10881  iooinsup  11326  isermulc2  11389  dvds2add  11873  dvds2sub  11874  dvdstr  11876  alzdvds  11901  divalg2  11972  lcmgcdlem  12120  lcmgcdeq  12126  isprm6  12190  pcqcl  12349  mgmplusf  12853  grpinva  12873  ismndd  12921  idmhm  12944  issubm2  12948  submid  12952  0mhm  12961  resmhm  12962  resmhm2  12963  resmhm2b  12964  mhmco  12965  mhmima  12966  grpinvcnv  13035  grpinvnzcl  13039  grpsubf  13046  imasgrp2  13075  qusgrp2  13078  mhmfmhm  13082  mulgnnsubcl  13099  mulgnn0z  13114  mulgnndir  13116  issubg4m  13157  isnsg3  13171  nsgid  13179  qusadd  13198  ghmmhm  13217  ghmmhmb  13218  idghm  13223  resghm  13224  ghmf1  13237  kerf1ghm  13238  qusghm  13246  ablnsg  13296  srgfcl  13352  srgmulgass  13368  srglmhm  13372  srgrmhm  13373  opprringbg  13455  mulgass3  13460  subrngringnsg  13577  issubrng2  13582  issubrg2  13613  islmodd  13634  lmodscaf  13651  lcomf  13668  rmodislmodlem  13691  issubrgd  13793  qusmul2  13868  crngridl  13869  qusmulrng  13871  psraddcl  13981  tgclb  14050  topbas  14052  neissex  14150  cnpnei  14204  txcnp  14256  psmetxrge0  14317  psmetlecl  14319  xmetlecl  14352  xmettpos  14355  elbl3ps  14379  elbl3  14380  metss  14479  comet  14484  bdxmet  14486  bdmet  14487  bl2ioo  14527  divcnap  14540  cncfcdm  14554  divccncfap  14562  dvrecap  14662  cosz12  14686