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  3282  opthpr  3790  sotric  4340  sotr2  4343  trsuc2OLD  4477  trsucss  4478  ordelinel  4491  ordunisuc2  4635  xpsspw  4797  relop  4834  fununi  5316  soisoi  5825  poxp  6227  soxp  6228  tfrlem11  6404  omordi  6564  om00  6573  odi  6577  omeulem2  6581  oewordi  6589  nnmordi  6629  omsmolem  6651  swoord2  6690  nneneq  7044  dffi3  7184  inf3lem6  7334  cantnfle  7372  cantnflem1  7391  cantnflem2  7392  r1sdom  7446  r1ord3g  7451  rankxplim3  7551  carddom2  7610  wdomnumr  7691  alephordi  7701  alephdom  7708  cardaleph  7716  cdainf  7818  cfsuc  7883  cfsmolem  7896  sornom  7903  fin23lem25  7950  fin1a2lem11  8036  fin1a2s  8040  zorn2lem7  8129  ttukeylem5  8140  alephval2  8194  fpwwe2lem13  8264  gchaclem  8292  gch2  8301  prub  8618  sqgt0sr  8728  1re  8837  lelttr  8912  ltletr  8913  letr  8914  mul0or  9408  prodgt0  9601  squeeze0  9659  sup2  9710  un0addcl  9997  un0mulcl  9998  nn0sub  10014  elnnz  10034  zindd  10113  rpneg  10383  xrlttri  10473  xrlelttr  10487  xrltletr  10488  xrletr  10489  qextlt  10530  qextle  10531  xmullem2  10585  xlemul1a  10608  xrsupexmnf  10623  xrinfmexpnf  10624  supxrun  10634  prunioo  10764  difreicc  10767  iccsplit  10768  uzsplit  10855  fzm1  10862  expcl2lem  11115  expeq0  11132  expnegz  11136  expaddz  11146  expmulz  11148  sqlecan  11209  facdiv  11300  facwordi  11302  bcpasc  11333  resqrex  11736  absexpz  11790  caubnd  11842  summo  12190  zsum  12191  rpnnen2  12504  ordvdsmul  12565  dvdsprime  12771  prmdvdsexpr  12795  prmfac1  12797  pythagtriplem2  12870  4sqlem11  13002  vdwlem6  13033  vdwlem9  13036  vdwlem13  13040  prmlem0  13107  xpscfv  13464  pleval2  14099  pltletr  14105  plelttr  14106  tsrlemax  14329  efgredlemc  15054  frgpuptinv  15080  lt6abl  15181  dmdprdsplit2lem  15280  drngmul0or  15533  lvecvs0or  15861  domneq0  16038  baspartn  16692  0top  16721  indistopon  16738  restntr  16912  cnindis  17020  cmpfi  17135  filcon  17578  ufprim  17604  ufildr  17626  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  ovolicc2lem3  18878  rolle  19337  dvivthlem1  19355  coeaddlem  19630  dgrco  19656  plymul0or  19661  aalioulem3  19714  cxpge0  20030  cxpmul2z  20038  cxpcn3lem  20087  scvxcvx  20280  sqf11  20377  ppiublem1  20441  lgsdir2lem2  20563  lgsqrlem2  20581  gxnn0neg  20930  gxnn0suc  20931  nvmul0or  21210  hvmul0or  21604  subfacp1lem4  23714  untsucf  24056  mulge0b  24086  dfon2lem6  24144  dftrpred3g  24236  wfrlem14  24269  wfrlem15  24270  nodenselem4  24338  broutsideof2  24745  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  lineunray  24770  lineelsb2  24771  hfun  24808  meran1  24850  ontgval  24870  ordcmp  24886  repfuntw  25160  vtarsuelt  25895  finminlem  26231  nn0prpw  26239  refssfne  26294  sdclem2  26452  fdc  26455  divrngidl  26653  fphpdo  26900  pellfundex  26971  jm2.19lem4  27085  jm2.26a  27093  f1omvdco2  27391  psgnunilem2  27418  rfcnnnub  27707  lkreqN  29360  cvrnbtwn4  29469  4atlem12  29801  elpaddn0  29989  paddasslem17  30025  paddidm  30030  pmapjoin  30041  llnexchb2  30058  dalawlem13  30072  dalawlem14  30073  dochkrshp4  31579  lcfl6  31690
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