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  4845  sotri  5183  fnfco  5564  mpoeq3dva  6152  fovcdmda  6233  ovelrn  6238  fnmpoovd  6451  nnmsucr  6761  fidifsnid  7173  exmidpw  7215  undiffi  7232  fidcenumlemim  7269  ltpopr  7962  ltexprlemdisj  7973  recexprlemdisj  7997  mul4  8459  add4  8488  2addsub  8541  addsubeq4  8542  subadd4  8571  muladd  8712  ltleadd  8775  divmulap  9007  divap0  9016  div23ap  9023  div12ap  9026  divsubdirap  9040  divcanap5  9046  divmuleqap  9049  divcanap6  9051  divdiv32ap  9052  div2subap  9169  letrp1  9180  lemul12b  9193  lediv1  9201  cju  9293  nndivre  9342  nndivtr  9348  nn0addge1  9613  nn0addge2  9614  peano2uz2  9757  uzind  9761  uzind3  9763  fzind  9765  fnn0ind  9766  uzind4  9997  qre  10034  irrmul  10057  rpdivcl  10090  rerpdivcl  10095  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  fzaddel  10475  fzrev  10501  frec2uzf1od  10856  expdivap  11040  fundm2domnop0  11314  swrdwrdsymbg  11450  ccatpfx  11487  swrdccat  11521  2shfti  11610  iooinsup  12059  isermulc2  12122  dvds2add  12608  dvds2sub  12609  dvdstr  12611  alzdvds  12637  divalg2  12709  lcmgcdlem  12871  lcmgcdeq  12877  isprm6  12942  pcqcl  13105  mgmplusf  13735  grpinva  13755  ismndd  13799  imasmnd2  13808  idmhm  13825  issubm2  13829  submid  13833  0mhm  13842  resmhm  13843  resmhm2  13844  resmhm2b  13845  mhmco  13846  mhmima  13847  gzsumwsubmcl  13850  gzsumwmhm  13852  grpinvcnv  13922  grpinvnzcl  13926  grpsubf  13933  imasgrp2  13962  qusgrp2  13965  mhmfmhm  13969  mulgnnsubcl  13986  mulgnn0z  14001  mulgnndir  14003  issubg4m  14045  isnsg3  14059  nsgid  14067  qusadd  14086  ghmmhm  14105  ghmmhmb  14106  idghm  14111  resghm  14112  ghmf1  14125  kerf1ghm  14126  qusghm  14134  ghmfghm  14179  invghm  14182  ablnsg  14187  srgfcl  14326  srgmulgass  14342  srglmhm  14346  srgrmhm  14347  ringlghm  14415  ringrghm  14416  opprringbg  14434  mulgass3  14440  isnzr2  14540  subrngringnsg  14562  issubrng2  14567  issubrg2  14598  domnmuln0  14631  islmodd  14678  lmodscaf  14696  lcomf  14713  rmodislmodlem  14736  issubrgd  14838  qusrhm  14914  qusmul2  14915  crngridl  14916  qusmulrng  14918  znidom  15041  asclghm  15074  asclrhm  15082  rnasclmulcl  15086  psraddcl  15120  tgclb  15215  topbas  15217  neissex  15315  cnpnei  15369  txcnp  15421  psmetxrge0  15482  psmetlecl  15484  xmetlecl  15517  xmettpos  15520  elbl3ps  15544  elbl3  15545  metss  15644  comet  15649  bdxmet  15651  bdmet  15652  bl2ioo  15700  divcnap  15715  cncfcdm  15732  divccncfap  15740  dvrecap  15863  dvmptfsum  15875  cosz12  15931  gausslemma2dlem1a  16275  usgredg2vlem1  16561  usgredg2vlem2  16562