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

Theorem orim1d 961
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 960 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 843
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 844
This theorem is referenced by:  pm2.38  964  pm2.8  968  pm2.73  969  pm2.74  970  pm2.82  971  moeq3  3706  unss1  4158  ordtri2or2  6284  gchor  10041  relin01  11156  icombl  24080  ioombl  24081  coltr  26347  frgrregorufrg  28020  cycpmco2  30690  fmlasuc  32518  satffunlem1lem2  32535  satffunlem2lem2  32538  naim1  33622  onsucconni  33670  dnibndlem13  33714  mblfinlem2  34798  leat3  36299  meetat2  36301  paddss1  36821
  Copyright terms: Public domain W3C validator