MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim12d Structured version   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  3966  prel12  3967  fr2nr  4552  ordtri3or  4605  suceloni  4785  ordunisuc2  4816  sossfld  5309  funun  5487  soisores  6039  fnse  6455  sorpsscmpl  6525  oaord  6782  omord2  6802  omcan  6804  oeord  6823  oecan  6824  nnaord  6854  nnmord  6867  omsmo  6889  swoer  6925  unxpwdom  7549  rankxplim3  7797  cdainflem  8063  ackbij2  8115  sornom  8149  fin23lem20  8209  fpwwe2lem10  8506  inatsk  8645  ltadd2  9169  ltord1  9545  ltmul1  9852  lt2msq  9886  xmullem2  10836  difreicc  11020  fzospliti  11157  om2uzlti  11282  om2uzlt2i  11283  om2uzf1oi  11285  absor  12097  ruclem12  12832  dvdslelem  12886  odd2np1lem  12899  odd2np1  12900  isprm6  13101  pythagtrip  13200  pc2dvds  13244  mreexexlem4d  13864  mreexexd  13865  irredrmul  15804  mplsubrglem  16494  znidomb  16834  ppttop  17063  filcon  17907  trufil  17934  ufildr  17955  plycj  20187  cosord  20426  logdivlt  20508  isosctrlem2  20655  atans2  20763  wilthlem2  20844  basellem3  20857  lgsdir2lem4  21102  pntpbnd1  21272  hiidge0  22592  chirredlem4  23888  ifbieq12d2  23994  disjxpin  24020  iocinif  24136  erdszelem11  24879  erdsze2lem2  24882  dfon2lem5  25406  trpredrec  25508  nofv  25604  axcontlem2  25896  axcontlem4  25898  btwnconn1lem14  26026  btwnconn2  26028  ispridlc  26671  rexzrexnn0  26855  pell14qrdich  26923  acongsym  27032  dvdsacongtr  27040  lcvexchlem4  29772  lcvexchlem5  29773  paddss1  30551  paddss2  30552
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