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

Theorem orim2d 880
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 878 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381
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 195  df-or 383  df-an 384
This theorem is referenced by:  orim2  881  pm2.82  892  poxp  7153  soxp  7154  relin01  10401  nneo  11293  uzp1  11553  vdwlem9  15477  dfcon2  20974  fin1aufil  21488  dgrlt  23743  aalioulem2  23809  aalioulem5  23812  aalioulem6  23813  aaliou  23814  sqff1o  24625  disjpreima  28585  disjdsct  28669  voliune  29425  volfiniune  29426  naim2  31361  paddss2  33925  lzunuz  36152  acongneg2  36365  nneom  42117
  Copyright terms: Public domain W3C validator