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

Theorem orim1d 964
 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 963 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 845 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 210  df-an 401  df-or 846 This theorem is referenced by:  pm2.38  967  pm2.8  971  pm2.73  972  pm2.74  973  pm2.82  974  moeq3  3627  unss1  4085  ordtri2or2  6263  gchor  10077  relin01  11192  icombl  24254  ioombl  24255  coltr  26530  frgrregorufrg  28200  cycpmco2  30916  fmlasuc  32854  satffunlem1lem2  32871  satffunlem2lem2  32874  naim1  34117  onsucconni  34165  dnibndlem13  34209  mblfinlem2  35365  leat3  36861  meetat2  36863  paddss1  37383
 Copyright terms: Public domain W3C validator