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

Theorem orim12d 699
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 698 . 2
41, 2, 3syl2anc 391 1
Colors of variables: wff set class
Syntax hints:   wi 4   wo 628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1d  700  orim2d  701  3orim123d  1214  19.33b2  1517  preq12b  3532  prel12  3533  funun  4887  nnsucelsuc  6009  nnaord  6018  nnmord  6026  swoer  6070  ltsopr  6569  cauappcvgprlemloc  6623  mulextsr1lem  6686  reapcotr  7362  apcotr  7371  mulext1  7376  mulext  7378  peano2z  8037  zeo  8099  uzm1  8259  eluzdc  8303  fzospliti  8782  frec2uzltd  8850  bj-findis  9409
  Copyright terms: Public domain W3C validator