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

Theorem orim12d 700
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 699 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 391 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 629
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 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1d  701  orim2d  702  3orim123d  1215  19.33b2  1520  preq12b  3541  prel12  3542  funun  4944  nnsucelsuc  6070  nnaord  6082  nnmord  6090  swoer  6134  fidceq  6330  fin0or  6343  ltsopr  6692  cauappcvgprlemloc  6748  caucvgprlemloc  6771  caucvgprprlemloc  6799  mulextsr1lem  6862  reapcotr  7587  apcotr  7596  mulext1  7601  mulext  7603  peano2z  8279  zeo  8341  uzm1  8501  eluzdc  8545  fzospliti  9030  frec2uzltd  9163  absext  9635  bj-findis  10077
  Copyright terms: Public domain W3C validator