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  4730  sotri  5062  fnfco  5429  mpoeq3dva  5983  fovcdmda  6064  ovelrn  6069  fnmpoovd  6270  nnmsucr  6543  fidifsnid  6929  exmidpw  6966  undiffi  6983  fidcenumlemim  7013  ltpopr  7657  ltexprlemdisj  7668  recexprlemdisj  7692  mul4  8153  add4  8182  2addsub  8235  addsubeq4  8236  subadd4  8265  muladd  8405  ltleadd  8467  divmulap  8696  divap0  8705  div23ap  8712  div12ap  8715  divsubdirap  8729  divcanap5  8735  divmuleqap  8738  divcanap6  8740  divdiv32ap  8741  div2subap  8858  letrp1  8869  lemul12b  8882  lediv1  8890  cju  8982  nndivre  9020  nndivtr  9026  nn0addge1  9289  nn0addge2  9290  peano2uz2  9427  uzind  9431  uzind3  9433  fzind  9435  fnn0ind  9436  uzind4  9656  qre  9693  irrmul  9715  rpdivcl  9748  rerpdivcl  9753  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  fzaddel  10128  fzrev  10153  frec2uzf1od  10480  expdivap  10664  2shfti  10978  iooinsup  11423  isermulc2  11486  dvds2add  11971  dvds2sub  11972  dvdstr  11974  alzdvds  11999  divalg2  12070  lcmgcdlem  12218  lcmgcdeq  12224  isprm6  12288  pcqcl  12447  mgmplusf  12952  grpinva  12972  ismndd  13021  idmhm  13044  issubm2  13048  submid  13052  0mhm  13061  resmhm  13062  resmhm2  13063  resmhm2b  13064  mhmco  13065  mhmima  13066  gsumwsubmcl  13071  gsumwmhm  13073  grpinvcnv  13143  grpinvnzcl  13147  grpsubf  13154  imasgrp2  13183  qusgrp2  13186  mhmfmhm  13190  mulgnnsubcl  13207  mulgnn0z  13222  mulgnndir  13224  issubg4m  13266  isnsg3  13280  nsgid  13288  qusadd  13307  ghmmhm  13326  ghmmhmb  13327  idghm  13332  resghm  13333  ghmf1  13346  kerf1ghm  13347  qusghm  13355  ghmfghm  13399  invghm  13402  ablnsg  13407  srgfcl  13472  srgmulgass  13488  srglmhm  13492  srgrmhm  13493  ringlghm  13560  ringrghm  13561  opprringbg  13579  mulgass3  13584  isnzr2  13683  subrngringnsg  13704  issubrng2  13709  issubrg2  13740  domnmuln0  13772  islmodd  13792  lmodscaf  13809  lcomf  13826  rmodislmodlem  13849  issubrgd  13951  qusrhm  14027  qusmul2  14028  crngridl  14029  qusmulrng  14031  znidom  14156  psraddcl  14175  tgclb  14244  topbas  14246  neissex  14344  cnpnei  14398  txcnp  14450  psmetxrge0  14511  psmetlecl  14513  xmetlecl  14546  xmettpos  14549  elbl3ps  14573  elbl3  14574  metss  14673  comet  14678  bdxmet  14680  bdmet  14681  bl2ioo  14729  divcnap  14744  cncfcdm  14761  divccncfap  14769  dvrecap  14892  dvmptfsum  14904  cosz12  14956  gausslemma2dlem1a  15215