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

Theorem orim2d 838
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
Ref Expression
orim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
orim2d  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )

Proof of Theorem orim2d
StepHypRef Expression
1 idd 24 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2orim12d 836 1  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368
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 185  df-or 370  df-an 371
This theorem is referenced by:  orim2  839  pm2.82  850  poxp  6892  soxp  6893  relin01  10073  nneo  10940  uzp1  11111  vdwlem9  14359  dfcon2  19683  fin1aufil  20165  dgrlt  22394  aalioulem2  22460  aalioulem5  22463  aalioulem6  22464  aaliou  22465  sqff1o  23181  disjpreima  27115  disjdsct  27190  voliune  27838  volfiniune  27839  naim2  29425  lzunuz  30303  acongneg2  30517  paddss2  34614
  Copyright terms: Public domain W3C validator