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

Theorem orim12d 776
 Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
orim12d.1
orim12d.2
Assertion
Ref Expression
orim12d

Proof of Theorem orim12d
StepHypRef Expression
1 orim12d.1 . 2
2 orim12d.2 . 2
3 pm3.48 775 . 2
41, 2, 3syl2anc 409 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  orim1d  777  orim2d  778  3orim123d  1302  19.33b2  1609  eqifdc  3539  preq12b  3733  prel12  3734  exmidsssnc  4163  funun  5211  nnsucelsuc  6431  nnaord  6449  nnmord  6457  swoer  6501  fidceq  6807  fin0or  6824  enomnilem  7064  exmidomni  7068  fodjuomnilemres  7074  ltsopr  7499  cauappcvgprlemloc  7555  caucvgprlemloc  7578  caucvgprprlemloc  7606  suplocexprlemloc  7624  mulextsr1lem  7683  suplocsrlemb  7709  axpre-suploclemres  7804  reapcotr  8456  apcotr  8465  mulext1  8470  mulext  8472  mul0eqap  8527  peano2z  9186  zeo  9252  uzm1  9452  eluzdc  9503  fzospliti  10057  frec2uzltd  10284  absext  10945  qabsor  10957  maxleast  11095  dvdslelemd  11716  odd2np1lem  11744  odd2np1  11745  isprm6  12001  ennnfonelemrnh  12117  dedekindeulemloc  12957  suplociccreex  12962  dedekindicclemloc  12966  ivthinclemloc  12979  cos11  13134  uzdcinzz  13331  bj-charfunr  13344  bj-findis  13513  nninfomnilem  13552  isomninnlem  13563
 Copyright terms: Public domain W3C validator