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  4802  sotri  5139  fnfco  5519  mpoeq3dva  6095  fovcdmda  6176  ovelrn  6181  fnmpoovd  6389  nnmsucr  6699  fidifsnid  7101  exmidpw  7143  undiffi  7160  fidcenumlemim  7194  ltpopr  7875  ltexprlemdisj  7886  recexprlemdisj  7910  mul4  8370  add4  8399  2addsub  8452  addsubeq4  8453  subadd4  8482  muladd  8622  ltleadd  8685  divmulap  8914  divap0  8923  div23ap  8930  div12ap  8933  divsubdirap  8947  divcanap5  8953  divmuleqap  8956  divcanap6  8958  divdiv32ap  8959  div2subap  9076  letrp1  9087  lemul12b  9100  lediv1  9108  cju  9200  nndivre  9238  nndivtr  9244  nn0addge1  9507  nn0addge2  9508  peano2uz2  9648  uzind  9652  uzind3  9654  fzind  9656  fnn0ind  9657  uzind4  9883  qre  9920  irrmul  9942  rpdivcl  9975  rerpdivcl  9980  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  fzaddel  10356  fzrev  10381  frec2uzf1od  10731  expdivap  10915  fundm2domnop0  11175  swrdwrdsymbg  11311  ccatpfx  11348  swrdccat  11382  2shfti  11471  iooinsup  11917  isermulc2  11980  dvds2add  12466  dvds2sub  12467  dvdstr  12469  alzdvds  12495  divalg2  12567  lcmgcdlem  12729  lcmgcdeq  12735  isprm6  12799  pcqcl  12959  mgmplusf  13529  grpinva  13549  ismndd  13600  imasmnd2  13615  idmhm  13632  issubm2  13636  submid  13640  0mhm  13649  resmhm  13650  resmhm2  13651  resmhm2b  13652  mhmco  13653  mhmima  13654  gsumwsubmcl  13659  gsumwmhm  13661  grpinvcnv  13731  grpinvnzcl  13735  grpsubf  13742  imasgrp2  13777  qusgrp2  13780  mhmfmhm  13784  mulgnnsubcl  13801  mulgnn0z  13816  mulgnndir  13818  issubg4m  13860  isnsg3  13874  nsgid  13882  qusadd  13901  ghmmhm  13920  ghmmhmb  13921  idghm  13926  resghm  13927  ghmf1  13940  kerf1ghm  13941  qusghm  13949  ghmfghm  13993  invghm  13996  ablnsg  14001  srgfcl  14067  srgmulgass  14083  srglmhm  14087  srgrmhm  14088  ringlghm  14155  ringrghm  14156  opprringbg  14174  mulgass3  14179  isnzr2  14279  subrngringnsg  14300  issubrng2  14305  issubrg2  14336  domnmuln0  14369  islmodd  14389  lmodscaf  14406  lcomf  14423  rmodislmodlem  14446  issubrgd  14548  qusrhm  14624  qusmul2  14625  crngridl  14626  qusmulrng  14628  znidom  14753  psraddcl  14781  tgclb  14876  topbas  14878  neissex  14976  cnpnei  15030  txcnp  15082  psmetxrge0  15143  psmetlecl  15145  xmetlecl  15178  xmettpos  15181  elbl3ps  15205  elbl3  15206  metss  15305  comet  15310  bdxmet  15312  bdmet  15313  bl2ioo  15361  divcnap  15376  cncfcdm  15393  divccncfap  15401  dvrecap  15524  dvmptfsum  15536  cosz12  15591  gausslemma2dlem1a  15877  usgredg2vlem1  16163  usgredg2vlem2  16164