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

Theorem orim2d 964
 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 962 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844 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 210  df-an 400  df-or 845 This theorem is referenced by:  orim2  965  pm2.82  973  poxp  7808  soxp  7809  relin01  11156  nneo  12057  uzp1  12270  vdwlem9  16318  dfconn2  22034  fin1aufil  22547  dgrlt  24873  aalioulem2  24939  aalioulem5  24942  aalioulem6  24943  aaliou  24944  sqff1o  25777  disjpreima  30357  disjdsct  30472  voliune  31613  volfiniune  31614  satfvsucsuc  32740  naim2  33866  paddss2  37133  lzunuz  39752  acongneg2  39961  nneom  44982
 Copyright terms: Public domain W3C validator