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

Theorem orim2d 962
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 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:  orim2  963  pm2.82  971  poxp  7818  soxp  7819  relin01  11158  nneo  12060  uzp1  12273  vdwlem9  16320  dfconn2  21962  fin1aufil  22475  dgrlt  24790  aalioulem2  24856  aalioulem5  24859  aalioulem6  24860  aaliou  24861  sqff1o  25692  disjpreima  30268  disjdsct  30370  voliune  31393  volfiniune  31394  satfvsucsuc  32515  naim2  33641  paddss2  36840  lzunuz  39249  acongneg2  39458  nneom  44489
  Copyright terms: Public domain W3C validator