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

Theorem orim12d 811
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
orim12d.1  |-  ( ph  ->  ( ps  ->  ch ) )
orim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
orim12d  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )

Proof of Theorem orim12d
StepHypRef Expression
1 orim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 orim12d.2 . 2  |-  ( ph  ->  ( th  ->  ta ) )
3 pm3.48 806 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ta ) )  ->  (
( ps  \/  th )  ->  ( ch  \/  ta ) ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  orim1d  812  orim2d  813  3orim123d  1260  preq12b  3825  prel12  3826  fr2nr  4408  ordtri3or  4461  suceloni  4641  ordunisuc2  4672  sossfld  5157  funun  5333  soisores  5866  fnse  6274  sorpsscmpl  6330  oaord  6587  omord2  6607  omcan  6609  oeord  6628  oecan  6629  nnaord  6659  nnmord  6672  omsmo  6694  swoer  6730  unxpwdom  7348  rankxplim3  7596  cdainflem  7862  ackbij2  7914  sornom  7948  fin23lem20  8008  fpwwe2lem10  8306  inatsk  8445  ltadd2  8969  ltord1  9344  ltmul1  9651  lt2msq  9685  xmullem2  10632  difreicc  10814  fzospliti  10945  om2uzlti  11060  om2uzlt2i  11061  om2uzf1oi  11063  absor  11832  ruclem12  12566  dvdslelem  12620  odd2np1lem  12633  odd2np1  12634  isprm6  12835  pythagtrip  12934  pc2dvds  12978  mreexexlem4d  13598  mreexexd  13599  irredrmul  15538  mplsubrglem  16232  znidomb  16571  ppttop  16800  filcon  17630  trufil  17657  ufildr  17678  plycj  19711  cosord  19947  logdivlt  20025  isosctrlem2  20172  atans2  20280  wilthlem2  20360  basellem3  20373  lgsdir2lem4  20618  pntpbnd1  20788  ex-natded5.13-2  20856  hiidge0  21732  chirredlem4  23028  ifbieq12d2  23145  iocinif  23291  erdszelem11  24016  erdsze2lem2  24019  dfon2lem5  24528  trpredrec  24626  nofv  24696  axcontlem2  24979  axcontlem4  24981  btwnconn1lem14  25109  btwnconn2  25111  ispridlc  25843  rexzrexnn0  26033  pell14qrdich  26102  acongsym  26211  dvdsacongtr  26219  lcvexchlem4  29045  lcvexchlem5  29046  paddss1  29824  paddss2  29825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator