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

Theorem orim12d 710
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 709 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 397 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  orim1d  711  orim2d  712  3orim123d  1226  19.33b2  1536  preq12b  3569  prel12  3570  funun  4972  nnsucelsuc  6101  nnaord  6113  nnmord  6121  swoer  6165  fidceq  6361  fin0or  6374  ltsopr  6752  cauappcvgprlemloc  6808  caucvgprlemloc  6831  caucvgprprlemloc  6859  mulextsr1lem  6922  reapcotr  7663  apcotr  7672  mulext1  7677  mulext  7679  peano2z  8338  zeo  8402  uzm1  8599  eluzdc  8644  fzospliti  9134  frec2uzltd  9353  absext  9890  qabsor  9902  dvdslelemd  10155  odd2np1lem  10183  odd2np1  10184  bj-findis  10491
  Copyright terms: Public domain W3C validator