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

Theorem orim2d 990
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 988 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 874
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 199  df-an 386  df-or 875
This theorem is referenced by:  orim2  991  pm2.82  999  poxp  7524  soxp  7525  relin01  10842  nneo  11747  uzp1  11961  vdwlem9  16023  dfconn2  21548  fin1aufil  22061  dgrlt  24360  aalioulem2  24426  aalioulem5  24429  aalioulem6  24430  aaliou  24431  sqff1o  25257  disjpreima  29906  disjdsct  29990  voliune  30800  volfiniune  30801  naim2  32889  paddss2  35831  lzunuz  38105  acongneg2  38317  nneom  43108
  Copyright terms: Public domain W3C validator