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

Theorem orim12d 736
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 735 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 404 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 665
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orim1d  737  orim2d  738  3orim123d  1257  19.33b2  1566  eqifdc  3429  preq12b  3620  prel12  3621  funun  5071  nnsucelsuc  6266  nnaord  6282  nnmord  6290  swoer  6334  fidceq  6639  fin0or  6656  enomnilem  6855  exmidomni  6859  fodjuomnilemres  6864  ltsopr  7216  cauappcvgprlemloc  7272  caucvgprlemloc  7295  caucvgprprlemloc  7323  mulextsr1lem  7386  reapcotr  8136  apcotr  8145  mulext1  8150  mulext  8152  peano2z  8847  zeo  8912  uzm1  9110  eluzdc  9158  fzospliti  9648  frec2uzltd  9871  absext  10557  qabsor  10569  maxleast  10707  dvdslelemd  11183  odd2np1lem  11211  odd2np1  11212  isprm6  11465  uzdcinzz  11971  bj-findis  12147  nninfomnilem  12182
  Copyright terms: Public domain W3C validator