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  3788  prel12  3789  fr2nr  4371  ordtri3or  4424  suceloni  4604  ordunisuc2  4635  sossfld  5120  funun  5296  soisores  5824  fnse  6232  sorpsscmpl  6288  oaord  6545  omord2  6565  omcan  6567  oeord  6586  oecan  6587  nnaord  6617  nnmord  6630  omsmo  6652  swoer  6688  unxpwdom  7303  rankxplim3  7551  cdainflem  7817  ackbij2  7869  sornom  7903  fin23lem20  7963  fpwwe2lem10  8261  inatsk  8400  ltadd2  8924  ltord1  9299  ltmul1  9606  lt2msq  9640  xmullem2  10585  difreicc  10767  fzospliti  10898  om2uzlti  11013  om2uzlt2i  11014  om2uzf1oi  11016  absor  11785  ruclem12  12519  dvdslelem  12573  odd2np1lem  12586  odd2np1  12587  isprm6  12788  pythagtrip  12887  pc2dvds  12931  mreexexlem4d  13549  mreexexd  13550  irredrmul  15489  mplsubrglem  16183  znidomb  16515  ppttop  16744  filcon  17578  trufil  17605  ufildr  17626  plycj  19658  cosord  19894  logdivlt  19972  isosctrlem2  20119  atans2  20227  wilthlem2  20307  basellem3  20320  lgsdir2lem4  20565  pntpbnd1  20735  ex-natded5.13-2  20803  hiidge0  21677  chirredlem4  22973  ifbieq12d2  23149  iocinif  23274  erdszelem11  23732  erdsze2lem2  23735  dfon2lem5  24143  trpredrec  24241  nofv  24311  axcontlem2  24593  axcontlem4  24595  btwnconn1lem14  24723  btwnconn2  24725  pdiveql  26168  ispridlc  26695  rexzrexnn0  26885  pell14qrdich  26954  acongsym  27063  dvdsacongtr  27071  lcvexchlem4  29227  lcvexchlem5  29228  paddss1  30006  paddss2  30007
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