MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaod Structured version   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  3453  opthpr  3976  sotric  4529  sotr2  4532  trsucss  4667  ordelinel  4680  ordunisuc2  4824  xpsspw  4986  relop  5023  fununi  5517  fnpr  5950  fnprOLD  5951  soisoi  6048  poxp  6458  soxp  6459  tfrlem11  6649  omordi  6809  om00  6818  odi  6822  omeulem2  6826  oewordi  6834  nnmordi  6874  omsmolem  6896  swoord2  6935  nneneq  7290  dffi3  7436  inf3lem6  7588  cantnfle  7626  cantnflem1  7645  cantnflem2  7646  r1sdom  7700  r1ord3g  7705  rankxplim3  7805  carddom2  7864  wdomnumr  7945  alephordi  7955  alephdom  7962  cardaleph  7970  cdainf  8072  cfsuc  8137  cfsmolem  8150  sornom  8157  fin23lem25  8204  fin1a2lem11  8290  fin1a2s  8294  zorn2lem7  8382  ttukeylem5  8393  alephval2  8447  fpwwe2lem13  8517  gchaclem  8545  gch2  8554  prub  8871  sqgt0sr  8981  1re  9090  lelttr  9165  ltletr  9166  letr  9167  mul0or  9662  prodgt0  9855  squeeze0  9913  sup2  9964  un0addcl  10253  un0mulcl  10254  nn0sub  10270  elnnz  10292  zindd  10371  rpneg  10641  xrlttri  10732  xrlelttr  10746  xrltletr  10747  xrletr  10748  qextlt  10789  qextle  10790  xmullem2  10844  xlemul1a  10867  xrsupexmnf  10883  xrinfmexpnf  10884  supxrun  10894  prunioo  11025  difreicc  11028  iccsplit  11029  uzsplit  11118  fzm1  11127  expcl2lem  11393  expeq0  11410  expnegz  11414  expaddz  11424  expmulz  11426  sqlecan  11487  facdiv  11578  facwordi  11580  bcpasc  11612  resqrex  12056  absexpz  12110  caubnd  12162  summo  12511  zsum  12512  rpnnen2  12825  ordvdsmul  12886  dvdsprime  13092  prmdvdsexpr  13116  prmfac1  13118  pythagtriplem2  13191  4sqlem11  13323  vdwlem6  13354  vdwlem9  13357  vdwlem13  13361  prmlem0  13428  xpscfv  13787  pleval2  14422  pltletr  14428  plelttr  14429  tsrlemax  14652  efgredlemc  15377  frgpuptinv  15403  lt6abl  15504  dmdprdsplit2lem  15603  drngmul0or  15856  lvecvs0or  16180  domneq0  16357  baspartn  17019  0top  17048  indistopon  17065  restntr  17246  cnindis  17356  cmpfi  17471  filcon  17915  ufprim  17941  ufildr  17963  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  ovolicc2lem3  19415  rolle  19874  dvivthlem1  19892  coeaddlem  20167  dgrco  20193  plymul0or  20198  aalioulem3  20251  cxpge0  20574  cxpmul2z  20582  cxpcn3lem  20631  scvxcvx  20824  sqf11  20922  ppiublem1  20986  lgsdir2lem2  21108  lgsqrlem2  21126  gxnn0neg  21851  gxnn0suc  21852  nvmul0or  22133  hvmul0or  22527  disjxpin  24028  sibfof  24654  subfacp1lem4  24869  untsucf  25159  mulge0b  25191  zprod  25263  dfon2lem6  25415  dftrpred3g  25511  wfrlem14  25551  wfrlem15  25552  nodenselem4  25639  broutsideof2  26056  btwnoutside  26059  broutsideof3  26060  outsideoftr  26063  lineunray  26081  lineelsb2  26082  meran1  26161  ontgval  26181  ordcmp  26197  mblfinlem2  26244  ovoliunnfl  26248  itg2addnclem  26256  finminlem  26321  nn0prpw  26326  refssfne  26374  sdclem2  26446  fdc  26449  divrngidl  26638  fphpdo  26878  pellfundex  26949  jm2.19lem4  27063  jm2.26a  27071  f1omvdco2  27368  psgnunilem2  27395  cshwssizelem4  28284  lkreqN  29968  cvrnbtwn4  30077  4atlem12  30409  elpaddn0  30597  paddasslem17  30633  paddidm  30638  pmapjoin  30649  llnexchb2  30666  dalawlem13  30680  dalawlem14  30681  dochkrshp4  32187  lcfl6  32298
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