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

Theorem orim12d 812
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 807 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ta ) )  ->  (
( ps  \/  th )  ->  ( ch  \/  ta ) ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  orim1d  813  orim2d  814  3orim123d  1262  preq12b  3918  prel12  3919  fr2nr  4503  ordtri3or  4556  suceloni  4735  ordunisuc2  4766  sossfld  5259  funun  5437  soisores  5988  fnse  6401  sorpsscmpl  6471  oaord  6728  omord2  6748  omcan  6750  oeord  6769  oecan  6770  nnaord  6800  nnmord  6813  omsmo  6835  swoer  6871  unxpwdom  7492  rankxplim3  7740  cdainflem  8006  ackbij2  8058  sornom  8092  fin23lem20  8152  fpwwe2lem10  8449  inatsk  8588  ltadd2  9112  ltord1  9487  ltmul1  9794  lt2msq  9828  xmullem2  10778  difreicc  10962  fzospliti  11097  om2uzlti  11219  om2uzlt2i  11220  om2uzf1oi  11222  absor  12034  ruclem12  12769  dvdslelem  12823  odd2np1lem  12836  odd2np1  12837  isprm6  13038  pythagtrip  13137  pc2dvds  13181  mreexexlem4d  13801  mreexexd  13802  irredrmul  15741  mplsubrglem  16431  znidomb  16767  ppttop  16996  filcon  17838  trufil  17865  ufildr  17886  plycj  20064  cosord  20303  logdivlt  20385  isosctrlem2  20532  atans2  20640  wilthlem2  20721  basellem3  20734  lgsdir2lem4  20979  pntpbnd1  21149  hiidge0  22450  chirredlem4  23746  ifbieq12d2  23848  iocinif  23982  erdszelem11  24668  erdsze2lem2  24671  dfon2lem5  25169  trpredrec  25267  nofv  25337  axcontlem2  25620  axcontlem4  25622  btwnconn1lem14  25750  btwnconn2  25752  ispridlc  26373  rexzrexnn0  26557  pell14qrdich  26625  acongsym  26734  dvdsacongtr  26742  lcvexchlem4  29154  lcvexchlem5  29155  paddss1  29933  paddss2  29934
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator