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

Theorem jaod 371
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)
Hypotheses
Ref Expression
jaod.1  |-  ( ph  ->  ( ps  ->  ch ) )
jaod.2  |-  ( ph  ->  ( th  ->  ch ) )
Assertion
Ref Expression
jaod  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)

Proof of Theorem jaod
StepHypRef Expression
1 jaod.1 . . . 4  |-  ( ph  ->  ( ps  ->  ch ) )
21com12 30 . . 3  |-  ( ps 
->  ( ph  ->  ch ) )
3 jaod.2 . . . 4  |-  ( ph  ->  ( th  ->  ch ) )
43com12 30 . . 3  |-  ( th 
->  ( ph  ->  ch ) )
52, 4jaoi 370 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 30 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359
This theorem is referenced by:  mpjaod  372  orel2  374  pm2.621  399  jaao  497  jaodan  762  pm2.63  765  ecase2d  908  ecase3d  911  dedlema  922  dedlemb  923  cad0  1410  psssstr  3455  opthpr  3978  sotric  4532  sotr2  4535  trsucss  4670  ordelinel  4683  ordunisuc2  4827  xpsspw  4989  relop  5026  fununi  5520  fnpr  5953  fnprOLD  5954  soisoi  6051  poxp  6461  soxp  6462  tfrlem11  6652  omordi  6812  om00  6821  odi  6825  omeulem2  6829  oewordi  6837  nnmordi  6877  omsmolem  6899  swoord2  6938  nneneq  7293  dffi3  7439  inf3lem6  7591  cantnfle  7629  cantnflem1  7648  cantnflem2  7649  r1sdom  7703  r1ord3g  7708  rankxplim3  7810  carddom2  7869  wdomnumr  7950  alephordi  7960  alephdom  7967  cardaleph  7975  cdainf  8077  cfsuc  8142  cfsmolem  8155  sornom  8162  fin23lem25  8209  fin1a2lem11  8295  fin1a2s  8299  zorn2lem7  8387  ttukeylem5  8398  alephval2  8452  fpwwe2lem13  8522  gch2  8555  gchaclem  8558  prub  8876  sqgt0sr  8986  1re  9095  lelttr  9170  ltletr  9171  letr  9172  mul0or  9667  prodgt0  9860  squeeze0  9918  sup2  9969  un0addcl  10258  un0mulcl  10259  nn0sub  10275  elnnz  10297  zindd  10376  rpneg  10646  xrlttri  10737  xrlelttr  10751  xrltletr  10752  xrletr  10753  qextlt  10794  qextle  10795  xmullem2  10849  xlemul1a  10872  xrsupexmnf  10888  xrinfmexpnf  10889  supxrun  10899  prunioo  11030  difreicc  11033  iccsplit  11034  uzsplit  11123  fzm1  11132  expcl2lem  11398  expeq0  11415  expnegz  11419  expaddz  11429  expmulz  11431  sqlecan  11492  facdiv  11583  facwordi  11585  bcpasc  11617  resqrex  12061  absexpz  12115  caubnd  12167  summo  12516  zsum  12517  rpnnen2  12830  ordvdsmul  12891  dvdsprime  13097  prmdvdsexpr  13121  prmfac1  13123  pythagtriplem2  13196  4sqlem11  13328  vdwlem6  13359  vdwlem9  13362  vdwlem13  13366  prmlem0  13433  xpscfv  13792  pleval2  14427  pltletr  14433  plelttr  14434  tsrlemax  14657  efgredlemc  15382  frgpuptinv  15408  lt6abl  15509  dmdprdsplit2lem  15608  drngmul0or  15861  lvecvs0or  16185  domneq0  16362  baspartn  17024  0top  17053  indistopon  17070  restntr  17251  cnindis  17361  cmpfi  17476  filcon  17920  ufprim  17946  ufildr  17968  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALTlem4  18086  ovolicc2lem3  19420  rolle  19879  dvivthlem1  19897  coeaddlem  20172  dgrco  20198  plymul0or  20203  aalioulem3  20256  cxpge0  20579  cxpmul2z  20587  cxpcn3lem  20636  scvxcvx  20829  sqf11  20927  ppiublem1  20991  lgsdir2lem2  21113  lgsqrlem2  21131  gxnn0neg  21856  gxnn0suc  21857  nvmul0or  22138  hvmul0or  22532  disjxpin  24033  sibfof  24659  subfacp1lem4  24874  untsucf  25164  mulge0b  25196  zprod  25268  dfon2lem6  25420  dftrpred3g  25516  wfrlem14  25556  wfrlem15  25557  nodenselem4  25644  broutsideof2  26061  btwnoutside  26064  broutsideof3  26065  outsideoftr  26068  lineunray  26086  lineelsb2  26087  meran1  26166  ontgval  26186  ordcmp  26202  mblfinlem2  26256  ovoliunnfl  26260  itg2addnclem  26270  finminlem  26335  nn0prpw  26340  refssfne  26388  sdclem2  26460  fdc  26463  divrngidl  26652  fphpdo  26892  pellfundex  26963  jm2.19lem4  27077  jm2.26a  27085  f1omvdco2  27382  psgnunilem2  27409  cshwssizelem4  28318  lkreqN  30042  cvrnbtwn4  30151  4atlem12  30483  elpaddn0  30671  paddasslem17  30707  paddidm  30712  pmapjoin  30723  llnexchb2  30740  dalawlem13  30754  dalawlem14  30755  dochkrshp4  32261  lcfl6  32372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator