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

Theorem jaod 369
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 27 . . 3  |-  ( ps 
->  ( ph  ->  ch ) )
3 jaod.2 . . . 4  |-  ( ph  ->  ( th  ->  ch ) )
43com12 27 . . 3  |-  ( th 
->  ( ph  ->  ch ) )
52, 4jaoi 368 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 27 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  mpjaod  370  orel2  372  pm2.621  397  jaao  495  jaodan  760  pm2.63  763  ecase2d  906  ecase3d  909  dedlema  920  dedlemb  921  cad0  1390  psssstr  3295  opthpr  3806  sotric  4356  sotr2  4359  trsuc2OLD  4493  trsucss  4494  ordelinel  4507  ordunisuc2  4651  xpsspw  4813  relop  4850  fununi  5332  soisoi  5841  poxp  6243  soxp  6244  tfrlem11  6420  omordi  6580  om00  6589  odi  6593  omeulem2  6597  oewordi  6605  nnmordi  6645  omsmolem  6667  swoord2  6706  nneneq  7060  dffi3  7200  inf3lem6  7350  cantnfle  7388  cantnflem1  7407  cantnflem2  7408  r1sdom  7462  r1ord3g  7467  rankxplim3  7567  carddom2  7626  wdomnumr  7707  alephordi  7717  alephdom  7724  cardaleph  7732  cdainf  7834  cfsuc  7899  cfsmolem  7912  sornom  7919  fin23lem25  7966  fin1a2lem11  8052  fin1a2s  8056  zorn2lem7  8145  ttukeylem5  8156  alephval2  8210  fpwwe2lem13  8280  gchaclem  8308  gch2  8317  prub  8634  sqgt0sr  8744  1re  8853  lelttr  8928  ltletr  8929  letr  8930  mul0or  9424  prodgt0  9617  squeeze0  9675  sup2  9726  un0addcl  10013  un0mulcl  10014  nn0sub  10030  elnnz  10050  zindd  10129  rpneg  10399  xrlttri  10489  xrlelttr  10503  xrltletr  10504  xrletr  10505  qextlt  10546  qextle  10547  xmullem2  10601  xlemul1a  10624  xrsupexmnf  10639  xrinfmexpnf  10640  supxrun  10650  prunioo  10780  difreicc  10783  iccsplit  10784  uzsplit  10871  fzm1  10878  expcl2lem  11131  expeq0  11148  expnegz  11152  expaddz  11162  expmulz  11164  sqlecan  11225  facdiv  11316  facwordi  11318  bcpasc  11349  resqrex  11752  absexpz  11806  caubnd  11858  summo  12206  zsum  12207  rpnnen2  12520  ordvdsmul  12581  dvdsprime  12787  prmdvdsexpr  12811  prmfac1  12813  pythagtriplem2  12886  4sqlem11  13018  vdwlem6  13049  vdwlem9  13052  vdwlem13  13056  prmlem0  13123  xpscfv  13480  pleval2  14115  pltletr  14121  plelttr  14122  tsrlemax  14345  efgredlemc  15070  frgpuptinv  15096  lt6abl  15197  dmdprdsplit2lem  15296  drngmul0or  15549  lvecvs0or  15877  domneq0  16054  baspartn  16708  0top  16737  indistopon  16754  restntr  16928  cnindis  17036  cmpfi  17151  filcon  17594  ufprim  17620  ufildr  17642  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  ovolicc2lem3  18894  rolle  19353  dvivthlem1  19371  coeaddlem  19646  dgrco  19672  plymul0or  19677  aalioulem3  19730  cxpge0  20046  cxpmul2z  20054  cxpcn3lem  20103  scvxcvx  20296  sqf11  20393  ppiublem1  20457  lgsdir2lem2  20579  lgsqrlem2  20597  gxnn0neg  20946  gxnn0suc  20947  nvmul0or  21226  hvmul0or  21620  subfacp1lem4  23729  untsucf  24071  mulge0b  24101  zprod  24160  dfon2lem6  24215  dftrpred3g  24307  wfrlem14  24340  wfrlem15  24341  nodenselem4  24409  broutsideof2  24817  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  lineunray  24842  lineelsb2  24843  hfun  24880  meran1  24922  ontgval  24942  ordcmp  24958  ovoliunnfl  25001  itg2addnclem  25003  repfuntw  25263  vtarsuelt  25998  finminlem  26334  nn0prpw  26342  refssfne  26397  sdclem2  26555  fdc  26558  divrngidl  26756  fphpdo  27003  pellfundex  27074  jm2.19lem4  27188  jm2.26a  27196  f1omvdco2  27494  psgnunilem2  27521  rfcnnnub  27810  lkreqN  29982  cvrnbtwn4  30091  4atlem12  30423  elpaddn0  30611  paddasslem17  30647  paddidm  30652  pmapjoin  30663  llnexchb2  30680  dalawlem13  30694  dalawlem14  30695  dochkrshp4  32201  lcfl6  32312
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
  Copyright terms: Public domain W3C validator