MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim1d Structured version   Visualization version   GIF version

Theorem orim1d 920
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
Ref Expression
orim1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
orim1d (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))

Proof of Theorem orim1d
StepHypRef Expression
1 orim1d.1 . 2 (𝜑 → (𝜓𝜒))
2 idd 24 . 2 (𝜑 → (𝜃𝜃))
31, 2orim12d 919 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385
This theorem is referenced by:  pm2.38  923  pm2.73  926  pm2.74  927  pm2.8  931  pm2.82  933  moeq3  3524  unss1  3925  ordtri2or2  5984  gchor  9641  relin01  10744  icombl  23532  ioombl  23533  coltr  25741  frgrregorufrg  27480  naim1  32690  onsucconni  32742  dnibndlem13  32786  mblfinlem2  33760  leat3  35085  meetat2  35087  paddss1  35606
  Copyright terms: Public domain W3C validator