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  8458  add4  8487  2addsub  8540  addsubeq4  8541  subadd4  8570  muladd  8711  ltleadd  8774  divmulap  9005  divap0  9014  div23ap  9021  div12ap  9024  divsubdirap  9038  divcanap5  9044  divmuleqap  9047  divcanap6  9049  divdiv32ap  9050  div2subap  9167  letrp1  9178  lemul12b  9191  lediv1  9199  cju  9291  nndivre  9340  nndivtr  9346  nn0addge1  9609  nn0addge2  9610  peano2uz2  9753  uzind  9757  uzind3  9759  fzind  9761  fnn0ind  9762  uzind4  9988  qre  10025  irrmul  10047  rpdivcl  10080  rerpdivcl  10085  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  fzaddel  10465  fzrev  10491  frec2uzf1od  10843  expdivap  11027  fundm2domnop0  11300  swrdwrdsymbg  11436  ccatpfx  11473  swrdccat  11507  2shfti  11596  iooinsup  12043  isermulc2  12106  dvds2add  12592  dvds2sub  12593  dvdstr  12595  alzdvds  12621  divalg2  12693  lcmgcdlem  12855  lcmgcdeq  12861  isprm6  12925  pcqcl  13085  mgmplusf  13686  grpinva  13706  ismndd  13750  imasmnd2  13759  idmhm  13776  issubm2  13780  submid  13784  0mhm  13793  resmhm  13794  resmhm2  13795  resmhm2b  13796  mhmco  13797  mhmima  13798  gzsumwsubmcl  13801  gzsumwmhm  13803  grpinvcnv  13873  grpinvnzcl  13877  grpsubf  13884  imasgrp2  13913  qusgrp2  13916  mhmfmhm  13920  mulgnnsubcl  13937  mulgnn0z  13952  mulgnndir  13954  issubg4m  13996  isnsg3  14010  nsgid  14018  qusadd  14037  ghmmhm  14056  ghmmhmb  14057  idghm  14062  resghm  14063  ghmf1  14076  kerf1ghm  14077  qusghm  14085  ghmfghm  14130  invghm  14133  ablnsg  14138  srgfcl  14277  srgmulgass  14293  srglmhm  14297  srgrmhm  14298  ringlghm  14366  ringrghm  14367  opprringbg  14385  mulgass3  14391  isnzr2  14491  subrngringnsg  14513  issubrng2  14518  issubrg2  14549  domnmuln0  14582  islmodd  14629  lmodscaf  14647  lcomf  14664  rmodislmodlem  14687  issubrgd  14789  qusrhm  14865  qusmul2  14866  crngridl  14867  qusmulrng  14869  znidom  14992  asclghm  15025  asclrhm  15033  rnasclmulcl  15037  psraddcl  15071  tgclb  15166  topbas  15168  neissex  15266  cnpnei  15320  txcnp  15372  psmetxrge0  15433  psmetlecl  15435  xmetlecl  15468  xmettpos  15471  elbl3ps  15495  elbl3  15496  metss  15595  comet  15600  bdxmet  15602  bdmet  15603  bl2ioo  15651  divcnap  15666  cncfcdm  15683  divccncfap  15691  dvrecap  15814  dvmptfsum  15826  cosz12  15881  gausslemma2dlem1a  16177  usgredg2vlem1  16463  usgredg2vlem2  16464