Theorem 3expb 1206

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

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

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 982

This theorem is referenced by:  3adant3r1  1214  3adant3r2  1215  3adant3r3  1216  3adant1l  1232  3adant1r  1233  mp3an1  1335  soinxp  4734  sotri  5066  fnfco  5435  mpoeq3dva  5990  fovcdmda  6071  ovelrn  6076  fnmpoovd  6282  nnmsucr  6555  fidifsnid  6941  exmidpw  6978  undiffi  6995  fidcenumlemim  7027  ltpopr  7679  ltexprlemdisj  7690  recexprlemdisj  7714  mul4  8175  add4  8204  2addsub  8257  addsubeq4  8258  subadd4  8287  muladd  8427  ltleadd  8490  divmulap  8719  divap0  8728  div23ap  8735  div12ap  8738  divsubdirap  8752  divcanap5  8758  divmuleqap  8761  divcanap6  8763  divdiv32ap  8764  div2subap  8881  letrp1  8892  lemul12b  8905  lediv1  8913  cju  9005  nndivre  9043  nndivtr  9049  nn0addge1  9312  nn0addge2  9313  peano2uz2  9450  uzind  9454  uzind3  9456  fzind  9458  fnn0ind  9459  uzind4  9679  qre  9716  irrmul  9738  rpdivcl  9771  rerpdivcl  9776  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  fzaddel  10151  fzrev  10176  frec2uzf1od  10515  expdivap  10699  2shfti  11013  iooinsup  11459  isermulc2  11522  dvds2add  12007  dvds2sub  12008  dvdstr  12010  alzdvds  12036  divalg2  12108  lcmgcdlem  12270  lcmgcdeq  12276  isprm6  12340  pcqcl  12500  mgmplusf  13068  grpinva  13088  ismndd  13139  imasmnd2  13154  idmhm  13171  issubm2  13175  submid  13179  0mhm  13188  resmhm  13189  resmhm2  13190  resmhm2b  13191  mhmco  13192  mhmima  13193  gsumwsubmcl  13198  gsumwmhm  13200  grpinvcnv  13270  grpinvnzcl  13274  grpsubf  13281  imasgrp2  13316  qusgrp2  13319  mhmfmhm  13323  mulgnnsubcl  13340  mulgnn0z  13355  mulgnndir  13357  issubg4m  13399  isnsg3  13413  nsgid  13421  qusadd  13440  ghmmhm  13459  ghmmhmb  13460  idghm  13465  resghm  13466  ghmf1  13479  kerf1ghm  13480  qusghm  13488  ghmfghm  13532  invghm  13535  ablnsg  13540  srgfcl  13605  srgmulgass  13621  srglmhm  13625  srgrmhm  13626  ringlghm  13693  ringrghm  13694  opprringbg  13712  mulgass3  13717  isnzr2  13816  subrngringnsg  13837  issubrng2  13842  issubrg2  13873  domnmuln0  13905  islmodd  13925  lmodscaf  13942  lcomf  13959  rmodislmodlem  13982  issubrgd  14084  qusrhm  14160  qusmul2  14161  crngridl  14162  qusmulrng  14164  znidom  14289  psraddcl  14308  tgclb  14385  topbas  14387  neissex  14485  cnpnei  14539  txcnp  14591  psmetxrge0  14652  psmetlecl  14654  xmetlecl  14687  xmettpos  14690  elbl3ps  14714  elbl3  14715  metss  14814  comet  14819  bdxmet  14821  bdmet  14822  bl2ioo  14870  divcnap  14885  cncfcdm  14902  divccncfap  14910  dvrecap  15033  dvmptfsum  15045  cosz12  15100  gausslemma2dlem1a  15383