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

Theorem orim1d 880
 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 879 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 196  df-or 384  df-an 385 This theorem is referenced by:  pm2.38  883  pm2.73  886  pm2.74  887  pm2.8  891  pm2.82  893  moeq3  3350  unss1  3744  ordtri2or2  5740  gchor  9328  relin01  10431  icombl  23139  ioombl  23140  coltr  25342  frgraregorufrg  26599  naim1  31554  onsucconi  31606  dnibndlem13  31650  mblfinlem2  32617  leat3  33600  meetat2  33602  paddss1  34121  frgrregorufrg  41505
 Copyright terms: Public domain W3C validator