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

Theorem jaod 370
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 29 . . 3  |-  ( ps 
->  ( ph  ->  ch ) )
3 jaod.2 . . . 4  |-  ( ph  ->  ( th  ->  ch ) )
43com12 29 . . 3  |-  ( th 
->  ( ph  ->  ch ) )
52, 4jaoi 369 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 29 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  mpjaod  371  orel2  373  pm2.621  398  jaao  496  jaodan  761  pm2.63  764  ecase2d  907  ecase3d  910  dedlema  921  dedlemb  922  cad0  1409  psssstr  3445  opthpr  3968  sotric  4521  sotr2  4524  trsucss  4658  ordelinel  4671  ordunisuc2  4815  xpsspw  4977  relop  5014  fununi  5508  fnpr  5941  fnprOLD  5942  soisoi  6039  poxp  6449  soxp  6450  tfrlem11  6640  omordi  6800  om00  6809  odi  6813  omeulem2  6817  oewordi  6825  nnmordi  6865  omsmolem  6887  swoord2  6926  nneneq  7281  dffi3  7427  inf3lem6  7577  cantnfle  7615  cantnflem1  7634  cantnflem2  7635  r1sdom  7689  r1ord3g  7694  rankxplim3  7794  carddom2  7853  wdomnumr  7934  alephordi  7944  alephdom  7951  cardaleph  7959  cdainf  8061  cfsuc  8126  cfsmolem  8139  sornom  8146  fin23lem25  8193  fin1a2lem11  8279  fin1a2s  8283  zorn2lem7  8371  ttukeylem5  8382  alephval2  8436  fpwwe2lem13  8506  gchaclem  8534  gch2  8543  prub  8860  sqgt0sr  8970  1re  9079  lelttr  9154  ltletr  9155  letr  9156  mul0or  9651  prodgt0  9844  squeeze0  9902  sup2  9953  un0addcl  10242  un0mulcl  10243  nn0sub  10259  elnnz  10281  zindd  10360  rpneg  10630  xrlttri  10721  xrlelttr  10735  xrltletr  10736  xrletr  10737  qextlt  10778  qextle  10779  xmullem2  10833  xlemul1a  10856  xrsupexmnf  10872  xrinfmexpnf  10873  supxrun  10883  prunioo  11014  difreicc  11017  iccsplit  11018  uzsplit  11106  fzm1  11115  expcl2lem  11381  expeq0  11398  expnegz  11402  expaddz  11412  expmulz  11414  sqlecan  11475  facdiv  11566  facwordi  11568  bcpasc  11600  resqrex  12044  absexpz  12098  caubnd  12150  summo  12499  zsum  12500  rpnnen2  12813  ordvdsmul  12874  dvdsprime  13080  prmdvdsexpr  13104  prmfac1  13106  pythagtriplem2  13179  4sqlem11  13311  vdwlem6  13342  vdwlem9  13345  vdwlem13  13349  prmlem0  13416  xpscfv  13775  pleval2  14410  pltletr  14416  plelttr  14417  tsrlemax  14640  efgredlemc  15365  frgpuptinv  15391  lt6abl  15492  dmdprdsplit2lem  15591  drngmul0or  15844  lvecvs0or  16168  domneq0  16345  baspartn  17007  0top  17036  indistopon  17053  restntr  17234  cnindis  17344  cmpfi  17459  filcon  17903  ufprim  17929  ufildr  17951  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALTlem4  18069  ovolicc2lem3  19403  rolle  19862  dvivthlem1  19880  coeaddlem  20155  dgrco  20181  plymul0or  20186  aalioulem3  20239  cxpge0  20562  cxpmul2z  20570  cxpcn3lem  20619  scvxcvx  20812  sqf11  20910  ppiublem1  20974  lgsdir2lem2  21096  lgsqrlem2  21114  gxnn0neg  21839  gxnn0suc  21840  nvmul0or  22121  hvmul0or  22515  disjxpin  24016  sibfof  24642  subfacp1lem4  24857  untsucf  25147  mulge0b  25179  zprod  25252  dfon2lem6  25399  dftrpred3g  25491  wfrlem14  25524  wfrlem15  25525  nodenselem4  25593  broutsideof2  26004  btwnoutside  26007  broutsideof3  26008  outsideoftr  26011  lineunray  26029  lineelsb2  26030  meran1  26109  ontgval  26129  ordcmp  26145  mblfinlem  26190  ovoliunnfl  26194  itg2addnclem  26202  finminlem  26258  nn0prpw  26263  refssfne  26311  sdclem2  26383  fdc  26386  divrngidl  26575  fphpdo  26815  pellfundex  26886  jm2.19lem4  27000  jm2.26a  27008  f1omvdco2  27306  psgnunilem2  27333  shwrdssizelem4  28170  lkreqN  29807  cvrnbtwn4  29916  4atlem12  30248  elpaddn0  30436  paddasslem17  30472  paddidm  30477  pmapjoin  30488  llnexchb2  30505  dalawlem13  30519  dalawlem14  30520  dochkrshp4  32026  lcfl6  32137
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
  Copyright terms: Public domain W3C validator