ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3expb Unicode version

Theorem 3expb 1204
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
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1202 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 257 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
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 980
This theorem is referenced by:  3adant3r1  1212  3adant3r2  1213  3adant3r3  1214  3adant1l  1230  3adant1r  1231  mp3an1  1324  soinxp  4692  sotri  5019  fnfco  5385  mpoeq3dva  5932  fovcdmda  6011  ovelrn  6016  fnmpoovd  6209  nnmsucr  6482  fidifsnid  6864  exmidpw  6901  undiffi  6917  fidcenumlemim  6944  ltpopr  7572  ltexprlemdisj  7583  recexprlemdisj  7607  mul4  8066  add4  8095  2addsub  8148  addsubeq4  8149  subadd4  8178  muladd  8318  ltleadd  8380  divmulap  8608  divap0  8617  div23ap  8624  div12ap  8627  divsubdirap  8641  divcanap5  8647  divmuleqap  8650  divcanap6  8652  divdiv32ap  8653  div2subap  8770  letrp1  8781  lemul12b  8794  lediv1  8802  cju  8894  nndivre  8931  nndivtr  8937  nn0addge1  9198  nn0addge2  9199  peano2uz2  9336  uzind  9340  uzind3  9342  fzind  9344  fnn0ind  9345  uzind4  9564  qre  9601  irrmul  9623  rpdivcl  9653  rerpdivcl  9658  iccshftr  9968  iccshftl  9970  iccdil  9972  icccntr  9974  fzaddel  10032  fzrev  10057  frec2uzf1od  10379  expdivap  10544  2shfti  10811  iooinsup  11256  isermulc2  11319  dvds2add  11803  dvds2sub  11804  dvdstr  11806  alzdvds  11830  divalg2  11901  lcmgcdlem  12047  lcmgcdeq  12053  isprm6  12117  pcqcl  12276  mgmplusf  12664  grprinvd  12684  ismndd  12717  idmhm  12737  issubm2  12741  submid  12745  0mhm  12750  mhmco  12751  mhmima  12752  grpinvcnv  12814  grpinvnzcl  12818  grpsubf  12825  mhmfmhm  12857  mulgnnsubcl  12871  mulgnn0z  12885  mulgnndir  12887  srgfcl  12969  srgmulgass  12985  srglmhm  12989  srgrmhm  12990  opprringbg  13062  mulgass3  13066  tgclb  13198  topbas  13200  neissex  13298  cnpnei  13352  txcnp  13404  psmetxrge0  13465  psmetlecl  13467  xmetlecl  13500  xmettpos  13503  elbl3ps  13527  elbl3  13528  metss  13627  comet  13632  bdxmet  13634  bdmet  13635  bl2ioo  13675  divcnap  13688  cncfcdm  13702  divccncfap  13710  dvrecap  13810  cosz12  13834
  Copyright terms: Public domain W3C validator