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

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

Proof of Theorem orim2d
StepHypRef Expression
1 idd 24 . 2 (𝜑 → (𝜃𝜃))
2 orim1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 2orim12d 901 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:  orim2  904  pm2.82  915  poxp  7334  soxp  7335  relin01  10590  nneo  11499  uzp1  11759  vdwlem9  15740  dfconn2  21270  fin1aufil  21783  dgrlt  24067  aalioulem2  24133  aalioulem5  24136  aalioulem6  24137  aaliou  24138  sqff1o  24953  disjpreima  29523  disjdsct  29608  voliune  30420  volfiniune  30421  naim2  32510  paddss2  35422  lzunuz  37648  acongneg2  37861  nneom  42646
  Copyright terms: Public domain W3C validator