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

Theorem 3expb 1182
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 1180 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 255 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  3adant3r1  1190  3adant3r2  1191  3adant3r3  1192  3adant1l  1208  3adant1r  1209  mp3an1  1302  soinxp  4609  sotri  4934  fnfco  5297  mpoeq3dva  5835  fovrnda  5914  ovelrn  5919  grprinvd  5966  fnmpoovd  6112  nnmsucr  6384  fidifsnid  6765  exmidpw  6802  undiffi  6813  fidcenumlemim  6840  ltpopr  7415  ltexprlemdisj  7426  recexprlemdisj  7450  mul4  7906  add4  7935  2addsub  7988  addsubeq4  7989  subadd4  8018  muladd  8158  ltleadd  8220  divmulap  8447  divap0  8456  div23ap  8463  div12ap  8466  divsubdirap  8480  divcanap5  8486  divmuleqap  8489  divcanap6  8491  divdiv32ap  8492  div2subap  8608  letrp1  8618  lemul12b  8631  lediv1  8639  cju  8731  nndivre  8768  nndivtr  8774  nn0addge1  9035  nn0addge2  9036  peano2uz2  9170  uzind  9174  uzind3  9176  fzind  9178  fnn0ind  9179  uzind4  9395  qre  9429  irrmul  9451  rpdivcl  9479  rerpdivcl  9484  iccshftr  9789  iccshftl  9791  iccdil  9793  icccntr  9795  fzaddel  9851  fzrev  9876  frec2uzf1od  10191  expdivap  10356  2shfti  10615  iooinsup  11058  isermulc2  11121  dvds2add  11538  dvds2sub  11539  dvdstr  11541  alzdvds  11563  divalg2  11634  lcmgcdlem  11769  lcmgcdeq  11775  isprm6  11836  tgclb  12248  topbas  12250  neissex  12348  cnpnei  12402  txcnp  12454  psmetxrge0  12515  psmetlecl  12517  xmetlecl  12550  xmettpos  12553  elbl3ps  12577  elbl3  12578  metss  12677  comet  12682  bdxmet  12684  bdmet  12685  bl2ioo  12725  divcnap  12738  cncffvrn  12752  divccncfap  12760  dvrecap  12860  cosz12  12883
  Copyright terms: Public domain W3C validator