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

Theorem orim2d 921
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 919 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  922  pm2.82  933  poxp  7457  soxp  7458  relin01  10744  nneo  11653  uzp1  11914  vdwlem9  15895  dfconn2  21424  fin1aufil  21937  dgrlt  24221  aalioulem2  24287  aalioulem5  24290  aalioulem6  24291  aaliou  24292  sqff1o  25107  disjpreima  29704  disjdsct  29789  voliune  30601  volfiniune  30602  naim2  32691  paddss2  35607  lzunuz  37833  acongneg2  38046  nneom  42831
  Copyright terms: Public domain W3C validator