Theorem 3expb 1228

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

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

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 1004

This theorem is referenced by:  3adant3r1  1236  3adant3r2  1237  3adant3r3  1238  3adant1l  1254  3adant1r  1255  mp3an1  1358  soinxp  4789  sotri  5124  fnfco  5502  mpoeq3dva  6074  fovcdmda  6155  ovelrn  6160  fnmpoovd  6367  nnmsucr  6642  fidifsnid  7041  exmidpw  7081  undiffi  7098  fidcenumlemim  7130  ltpopr  7793  ltexprlemdisj  7804  recexprlemdisj  7828  mul4  8289  add4  8318  2addsub  8371  addsubeq4  8372  subadd4  8401  muladd  8541  ltleadd  8604  divmulap  8833  divap0  8842  div23ap  8849  div12ap  8852  divsubdirap  8866  divcanap5  8872  divmuleqap  8875  divcanap6  8877  divdiv32ap  8878  div2subap  8995  letrp1  9006  lemul12b  9019  lediv1  9027  cju  9119  nndivre  9157  nndivtr  9163  nn0addge1  9426  nn0addge2  9427  peano2uz2  9565  uzind  9569  uzind3  9571  fzind  9573  fnn0ind  9574  uzind4  9795  qre  9832  irrmul  9854  rpdivcl  9887  rerpdivcl  9892  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  fzrev  10292  frec2uzf1od  10640  expdivap  10824  fundm2domnop0  11080  swrdwrdsymbg  11212  ccatpfx  11249  swrdccat  11283  2shfti  11358  iooinsup  11804  isermulc2  11867  dvds2add  12352  dvds2sub  12353  dvdstr  12355  alzdvds  12381  divalg2  12453  lcmgcdlem  12615  lcmgcdeq  12621  isprm6  12685  pcqcl  12845  mgmplusf  13415  grpinva  13435  ismndd  13486  imasmnd2  13501  idmhm  13518  issubm2  13522  submid  13526  0mhm  13535  resmhm  13536  resmhm2  13537  resmhm2b  13538  mhmco  13539  mhmima  13540  gsumwsubmcl  13545  gsumwmhm  13547  grpinvcnv  13617  grpinvnzcl  13621  grpsubf  13628  imasgrp2  13663  qusgrp2  13666  mhmfmhm  13670  mulgnnsubcl  13687  mulgnn0z  13702  mulgnndir  13704  issubg4m  13746  isnsg3  13760  nsgid  13768  qusadd  13787  ghmmhm  13806  ghmmhmb  13807  idghm  13812  resghm  13813  ghmf1  13826  kerf1ghm  13827  qusghm  13835  ghmfghm  13879  invghm  13882  ablnsg  13887  srgfcl  13952  srgmulgass  13968  srglmhm  13972  srgrmhm  13973  ringlghm  14040  ringrghm  14041  opprringbg  14059  mulgass3  14064  isnzr2  14164  subrngringnsg  14185  issubrng2  14190  issubrg2  14221  domnmuln0  14253  islmodd  14273  lmodscaf  14290  lcomf  14307  rmodislmodlem  14330  issubrgd  14432  qusrhm  14508  qusmul2  14509  crngridl  14510  qusmulrng  14512  znidom  14637  psraddcl  14660  tgclb  14755  topbas  14757  neissex  14855  cnpnei  14909  txcnp  14961  psmetxrge0  15022  psmetlecl  15024  xmetlecl  15057  xmettpos  15060  elbl3ps  15084  elbl3  15085  metss  15184  comet  15189  bdxmet  15191  bdmet  15192  bl2ioo  15240  divcnap  15255  cncfcdm  15272  divccncfap  15280  dvrecap  15403  dvmptfsum  15415  cosz12  15470  gausslemma2dlem1a  15753  usgredg2vlem1  16036  usgredg2vlem2  16037