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

Theorem orim1d 959
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 958 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 208  df-an 397  df-or 842
This theorem is referenced by:  pm2.38  962  pm2.8  966  pm2.73  967  pm2.74  968  pm2.82  969  moeq3  3700  unss1  4152  ordtri2or2  6280  gchor  10037  relin01  11152  icombl  24092  ioombl  24093  coltr  26360  frgrregorufrg  28032  cycpmco2  30702  fmlasuc  32530  satffunlem1lem2  32547  satffunlem2lem2  32550  naim1  33634  onsucconni  33682  dnibndlem13  33726  mblfinlem2  34811  leat3  36311  meetat2  36313  paddss1  36833
  Copyright terms: Public domain W3C validator