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  6765  fidifsnid  7177  exmidpw  7219  undiffi  7236  fidcenumlemim  7274  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  peano2uz2  9764  uzind  9768  uzind3  9770  fzind  9772  fnn0ind  9773  uzind4  10004  qre  10041  irrmul  10064  rpdivcl  10097  rerpdivcl  10102  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzaddel  10482  fzrev  10508  frec2uzf1od  10864  expdivap  11048  fundm2domnop0  11322  swrdwrdsymbg  11458  ccatpfx  11495  swrdccat  11529  2shfti  11618  iooinsup  12068  isermulc2  12131  dvds2add  12617  dvds2sub  12618  dvdstr  12620  alzdvds  12646  divalg2  12718  lcmgcdlem  12880  lcmgcdeq  12886  isprm6  12951  pcqcl  13114  mgmplusf  13745  grpinva  13765  ismndd  13809  imasmnd2  13818  idmhm  13835  issubm2  13839  submid  13843  0mhm  13852  resmhm  13853  resmhm2  13854  resmhm2b  13855  mhmco  13856  mhmima  13857  gzsumwsubmcl  13860  gzsumwmhm  13862  grpinvcnv  13932  grpinvnzcl  13936  grpsubf  13943  imasgrp2  13972  qusgrp2  13975  mhmfmhm  13979  mulgnnsubcl  13996  mulgnn0z  14011  mulgnndir  14013  issubg4m  14055  isnsg3  14069  nsgid  14077  qusadd  14096  ghmmhm  14115  ghmmhmb  14116  idghm  14121  resghm  14122  ghmf1  14135  kerf1ghm  14136  qusghm  14144  ghmfghm  14220  invghm  14223  ablnsg  14228  srgfcl  14384  srgmulgass  14400  srglmhm  14404  srgrmhm  14405  ringlghm  14473  ringrghm  14474  opprringbg  14494  mulgass3  14500  isnzr2  14600  subrngringnsg  14622  issubrng2  14627  issubrg2  14658  domnmuln0  14691  islmodd  14738  lmodscaf  14756  lcomf  14773  rmodislmodlem  14796  issubrgd  14898  qusrhm  14974  qusmul2  14975  crngridl  14976  qusmulrng  14978  znidom  15101  asclghm  15134  asclrhm  15142  rnasclmulcl  15146  psraddcl  15184  tgclb  15291  topbas  15293  neissex  15391  cnpnei  15445  txcnp  15497  psmetxrge0  15558  psmetlecl  15560  xmetlecl  15593  xmettpos  15596  elbl3ps  15620  elbl3  15621  metss  15720  comet  15725  bdxmet  15727  bdmet  15728  bl2ioo  15776  divcnap  15791  cncfcdm  15808  divccncfap  15816  dvrecap  15939  dvmptfsum  15951  cosz12  16007  gausslemma2dlem1a  16382  usgredg2vlem1  16668  usgredg2vlem2  16669