Theorem 3expb 1235

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3adant3r1  1243  3adant3r2  1244  3adant3r3  1245  3adant1l  1261  3adant1r  1262  mp3an1  1365  soinxp  4847  sotri  5186  fnfco  5567  mpoeq3dva  6155  fovcdmda  6236  ovelrn  6241  fnmpoovd  6455  nnmsucr  6766  fidifsnid  7179  exmidpw  7221  undiffi  7238  fidcenumlemim  7276  ltpopr  7968  ltexprlemdisj  7979  recexprlemdisj  8003  mul4  8465  add4  8494  2addsub  8547  addsubeq4  8548  subadd4  8577  muladd  8718  ltleadd  8781  divmulap  9013  divap0  9022  div23ap  9029  div12ap  9032  divsubdirap  9046  divcanap5  9052  divmuleqap  9055  divcanap6  9057  divdiv32ap  9058  div2subap  9175  letrp1  9186  lemul12b  9199  lediv1  9207  cju  9299  nndivre  9349  nndivtr  9355  nn0addge1  9620  nn0addge2  9621  fcdmnn0fsuppfi  9743  peano2uz2  9763  uzind  9767  uzind3  9769  fzind  9771  fnn0ind  9772  uzind4  10003  qre  10040  irrmul  10063  rpdivcl  10096  rerpdivcl  10101  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  fzaddel  10481  fzrev  10507  frec2uzf1od  10863  expdivap  11047  fundm2domnop0  11321  swrdwrdsymbg  11457  ccatpfx  11494  swrdccat  11528  2shfti  11617  iooinsup  12067  isermulc2  12130  dvds2add  12616  dvds2sub  12617  dvdstr  12619  alzdvds  12645  divalg2  12717  lcmgcdlem  12879  lcmgcdeq  12885  isprm6  12950  pcqcl  13113  mgmplusf  13744  grpinva  13764  ismndd  13808  imasmnd2  13817  idmhm  13834  issubm2  13838  submid  13842  0mhm  13851  resmhm  13852  resmhm2  13853  resmhm2b  13854  mhmco  13855  mhmima  13856  gzsumwsubmcl  13859  gzsumwmhm  13861  grpinvcnv  13931  grpinvnzcl  13935  grpsubf  13942  imasgrp2  13971  qusgrp2  13974  mhmfmhm  13978  mulgnnsubcl  13995  mulgnn0z  14010  mulgnndir  14012  issubg4m  14054  isnsg3  14068  nsgid  14076  qusadd  14095  ghmmhm  14114  ghmmhmb  14115  idghm  14120  resghm  14121  ghmf1  14134  kerf1ghm  14135  qusghm  14143  ghmfghm  14219  invghm  14222  ablnsg  14227  srgfcl  14383  srgmulgass  14399  srglmhm  14403  srgrmhm  14404  ringlghm  14472  ringrghm  14473  opprringbg  14493  mulgass3  14499  isnzr2  14599  subrngringnsg  14621  issubrng2  14626  issubrg2  14657  domnmuln0  14690  islmodd  14737  lmodscaf  14755  lcomf  14772  rmodislmodlem  14795  issubrgd  14897  qusrhm  14973  qusmul2  14974  crngridl  14975  qusmulrng  14977  znidom  15100  asclghm  15133  asclrhm  15141  rnasclmulcl  15145  psraddcl  15193  tgclb  15308  topbas  15310  neissex  15408  cnpnei  15462  txcnp  15514  psmetxrge0  15575  psmetlecl  15577  xmetlecl  15610  xmettpos  15613  elbl3ps  15637  elbl3  15638  metss  15737  comet  15742  bdxmet  15744  bdmet  15745  bl2ioo  15793  divcnap  15808  cncfcdm  15825  divccncfap  15833  dvrecap  15956  dvmptfsum  15968  cosz12  16024  gausslemma2dlem1a  16399  usgredg2vlem1  16685  usgredg2vlem2  16686