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

Theorem orim2d 965
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 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 206  df-an 397  df-or 846
This theorem is referenced by:  orim2  966  pm2.82  974  poxp  8059  soxp  8060  relin01  11678  nneo  12586  uzp1  12803  vdwlem9  16860  dfconn2  22768  fin1aufil  23281  dgrlt  25625  aalioulem2  25691  aalioulem5  25694  aalioulem6  25695  aaliou  25696  sqff1o  26529  disjpreima  31500  disjdsct  31612  voliune  32819  volfiniune  32820  satfvsucsuc  33950  naim2  34853  paddss2  38272  lzunuz  41069  acongneg2  41279  nneom  46585
  Copyright terms: Public domain W3C validator