Theorem 3expb 1231

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

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

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 1007

This theorem is referenced by:  3adant3r1  1239  3adant3r2  1240  3adant3r3  1241  3adant1l  1257  3adant1r  1258  mp3an1  1361  soinxp  4825  sotri  5163  fnfco  5544  mpoeq3dva  6125  fovcdmda  6206  ovelrn  6211  fnmpoovd  6424  nnmsucr  6734  fidifsnid  7139  exmidpw  7181  undiffi  7198  fidcenumlemim  7235  ltpopr  7926  ltexprlemdisj  7937  recexprlemdisj  7961  mul4  8421  add4  8450  2addsub  8503  addsubeq4  8504  subadd4  8533  muladd  8674  ltleadd  8737  divmulap  8966  divap0  8975  div23ap  8982  div12ap  8985  divsubdirap  8999  divcanap5  9005  divmuleqap  9008  divcanap6  9010  divdiv32ap  9011  div2subap  9128  letrp1  9139  lemul12b  9152  lediv1  9160  cju  9252  nndivre  9290  nndivtr  9296  nn0addge1  9559  nn0addge2  9560  peano2uz2  9703  uzind  9707  uzind3  9709  fzind  9711  fnn0ind  9712  uzind4  9938  qre  9975  irrmul  9997  rpdivcl  10030  rerpdivcl  10035  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzaddel  10414  fzrev  10440  frec2uzf1od  10792  expdivap  10976  fundm2domnop0  11245  swrdwrdsymbg  11381  ccatpfx  11418  swrdccat  11452  2shfti  11541  iooinsup  11987  isermulc2  12050  dvds2add  12536  dvds2sub  12537  dvdstr  12539  alzdvds  12565  divalg2  12637  lcmgcdlem  12799  lcmgcdeq  12805  isprm6  12869  pcqcl  13029  mgmplusf  13629  grpinva  13649  ismndd  13698  imasmnd2  13707  idmhm  13724  issubm2  13728  submid  13732  0mhm  13741  resmhm  13742  resmhm2  13743  resmhm2b  13744  mhmco  13745  mhmima  13746  gsumwsubmcl  13751  gsumwmhm  13753  grpinvcnv  13823  grpinvnzcl  13827  grpsubf  13834  imasgrp2  13863  qusgrp2  13866  mhmfmhm  13870  mulgnnsubcl  13887  mulgnn0z  13902  mulgnndir  13904  issubg4m  13946  isnsg3  13960  nsgid  13968  qusadd  13987  ghmmhm  14006  ghmmhmb  14007  idghm  14012  resghm  14013  ghmf1  14026  kerf1ghm  14027  qusghm  14035  ghmfghm  14079  invghm  14082  ablnsg  14087  srgfcl  14216  srgmulgass  14232  srglmhm  14236  srgrmhm  14237  ringlghm  14304  ringrghm  14305  opprringbg  14323  mulgass3  14329  isnzr2  14429  subrngringnsg  14451  issubrng2  14456  issubrg2  14487  domnmuln0  14520  islmodd  14567  lmodscaf  14584  lcomf  14601  rmodislmodlem  14624  issubrgd  14726  qusrhm  14802  qusmul2  14803  crngridl  14804  qusmulrng  14806  znidom  14931  psraddcl  14961  tgclb  15056  topbas  15058  neissex  15156  cnpnei  15210  txcnp  15262  psmetxrge0  15323  psmetlecl  15325  xmetlecl  15358  xmettpos  15361  elbl3ps  15385  elbl3  15386  metss  15485  comet  15490  bdxmet  15492  bdmet  15493  bl2ioo  15541  divcnap  15556  cncfcdm  15573  divccncfap  15581  dvrecap  15704  dvmptfsum  15716  cosz12  15771  gausslemma2dlem1a  16057  usgredg2vlem1  16343  usgredg2vlem2  16344