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  4733  sotri  5065  fnfco  5432  mpoeq3dva  5986  fovcdmda  6067  ovelrn  6072  fnmpoovd  6273  nnmsucr  6546  fidifsnid  6932  exmidpw  6969  undiffi  6986  fidcenumlemim  7018  ltpopr  7662  ltexprlemdisj  7673  recexprlemdisj  7697  mul4  8158  add4  8187  2addsub  8240  addsubeq4  8241  subadd4  8270  muladd  8410  ltleadd  8473  divmulap  8702  divap0  8711  div23ap  8718  div12ap  8721  divsubdirap  8735  divcanap5  8741  divmuleqap  8744  divcanap6  8746  divdiv32ap  8747  div2subap  8864  letrp1  8875  lemul12b  8888  lediv1  8896  cju  8988  nndivre  9026  nndivtr  9032  nn0addge1  9295  nn0addge2  9296  peano2uz2  9433  uzind  9437  uzind3  9439  fzind  9441  fnn0ind  9442  uzind4  9662  qre  9699  irrmul  9721  rpdivcl  9754  rerpdivcl  9759  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  fzaddel  10134  fzrev  10159  frec2uzf1od  10498  expdivap  10682  2shfti  10996  iooinsup  11442  isermulc2  11505  dvds2add  11990  dvds2sub  11991  dvdstr  11993  alzdvds  12019  divalg2  12091  lcmgcdlem  12245  lcmgcdeq  12251  isprm6  12315  pcqcl  12475  mgmplusf  13009  grpinva  13029  ismndd  13078  idmhm  13101  issubm2  13105  submid  13109  0mhm  13118  resmhm  13119  resmhm2  13120  resmhm2b  13121  mhmco  13122  mhmima  13123  gsumwsubmcl  13128  gsumwmhm  13130  grpinvcnv  13200  grpinvnzcl  13204  grpsubf  13211  imasgrp2  13240  qusgrp2  13243  mhmfmhm  13247  mulgnnsubcl  13264  mulgnn0z  13279  mulgnndir  13281  issubg4m  13323  isnsg3  13337  nsgid  13345  qusadd  13364  ghmmhm  13383  ghmmhmb  13384  idghm  13389  resghm  13390  ghmf1  13403  kerf1ghm  13404  qusghm  13412  ghmfghm  13456  invghm  13459  ablnsg  13464  srgfcl  13529  srgmulgass  13545  srglmhm  13549  srgrmhm  13550  ringlghm  13617  ringrghm  13618  opprringbg  13636  mulgass3  13641  isnzr2  13740  subrngringnsg  13761  issubrng2  13766  issubrg2  13797  domnmuln0  13829  islmodd  13849  lmodscaf  13866  lcomf  13883  rmodislmodlem  13906  issubrgd  14008  qusrhm  14084  qusmul2  14085  crngridl  14086  qusmulrng  14088  znidom  14213  psraddcl  14232  tgclb  14301  topbas  14303  neissex  14401  cnpnei  14455  txcnp  14507  psmetxrge0  14568  psmetlecl  14570  xmetlecl  14603  xmettpos  14606  elbl3ps  14630  elbl3  14631  metss  14730  comet  14735  bdxmet  14737  bdmet  14738  bl2ioo  14786  divcnap  14801  cncfcdm  14818  divccncfap  14826  dvrecap  14949  dvmptfsum  14961  cosz12  15016  gausslemma2dlem1a  15299