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  3804  prel12  3805  fr2nr  4387  ordtri3or  4440  suceloni  4620  ordunisuc2  4651  sossfld  5136  funun  5312  soisores  5840  fnse  6248  sorpsscmpl  6304  oaord  6561  omord2  6581  omcan  6583  oeord  6602  oecan  6603  nnaord  6633  nnmord  6646  omsmo  6668  swoer  6704  unxpwdom  7319  rankxplim3  7567  cdainflem  7833  ackbij2  7885  sornom  7919  fin23lem20  7979  fpwwe2lem10  8277  inatsk  8416  ltadd2  8940  ltord1  9315  ltmul1  9622  lt2msq  9656  xmullem2  10601  difreicc  10783  fzospliti  10914  om2uzlti  11029  om2uzlt2i  11030  om2uzf1oi  11032  absor  11801  ruclem12  12535  dvdslelem  12589  odd2np1lem  12602  odd2np1  12603  isprm6  12804  pythagtrip  12903  pc2dvds  12947  mreexexlem4d  13565  mreexexd  13566  irredrmul  15505  mplsubrglem  16199  znidomb  16531  ppttop  16760  filcon  17594  trufil  17621  ufildr  17642  plycj  19674  cosord  19910  logdivlt  19988  isosctrlem2  20135  atans2  20243  wilthlem2  20323  basellem3  20336  lgsdir2lem4  20581  pntpbnd1  20751  ex-natded5.13-2  20819  hiidge0  21693  chirredlem4  22989  ifbieq12d2  23165  iocinif  23289  erdszelem11  23747  erdsze2lem2  23750  dfon2lem5  24214  trpredrec  24312  nofv  24382  axcontlem2  24665  axcontlem4  24667  btwnconn1lem14  24795  btwnconn2  24797  pdiveql  26271  ispridlc  26798  rexzrexnn0  26988  pell14qrdich  27057  acongsym  27166  dvdsacongtr  27174  lcvexchlem4  29849  lcvexchlem5  29850  paddss1  30628  paddss2  30629
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