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

Theorem jaod 380
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)
Hypotheses
Ref Expression
jaod.1
jaod.2
Assertion
Ref Expression
jaod

Proof of Theorem jaod
StepHypRef Expression
1 jaod.1 . . . 4
21com12 31 . . 3
3 jaod.2 . . . 4
43com12 31 . . 3
52, 4jaoi 379 . 2
65com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  mpjaod  381  orel2  383  pm2.621  408  jaao  509  jaodan  785  pm2.63  788  ecase2d  940  ecase3d  943  dedlema  954  dedlemb  955  cad0  1467  psssstr  3609  opthpr  4208  sotric  4831  sotr2  4834  trsucss  4968  ordelinel  4981  xpsspw  5121  relop  5158  fununi  5659  fnprb  6129  fnprOLD  6130  soisoi  6224  ordunisuc2  6679  poxp  6912  soxp  6913  tfrlem11  7076  omordi  7234  om00  7243  odi  7247  omeulem2  7251  oewordi  7259  nnmordi  7299  omsmolem  7321  swoord2  7360  nneneq  7720  dffi3  7911  inf3lem6  8071  cantnfle  8111  cantnflem1  8129  cantnflem2  8130  cantnfleOLD  8141  cantnflem1OLD  8152  r1sdom  8213  r1ord3g  8218  rankxplim3  8320  carddom2  8379  wdomnumr  8466  alephordi  8476  alephdom  8483  cardaleph  8491  cdainf  8593  cfsuc  8658  cfsmolem  8671  sornom  8678  fin23lem25  8725  fin1a2lem11  8811  fin1a2s  8815  zorn2lem7  8903  ttukeylem5  8914  alephval2  8968  fpwwe2lem13  9041  gch2  9074  gchaclem  9077  prub  9393  sqgt0sr  9504  1re  9616  lelttr  9696  ltletr  9697  letr  9699  mul0or  10214  prodgt0  10412  mulge0b  10437  squeeze0  10473  sup2  10524  un0addcl  10854  un0mulcl  10855  nn0sub  10871  elnnz  10899  zindd  10990  rpneg  11278  xrlttri  11374  xrlelttr  11388  xrltletr  11389  xrletr  11390  qextlt  11431  qextle  11432  xmullem2  11486  xlemul1a  11509  xrsupexmnf  11525  xrinfmexpnf  11526  supxrun  11536  prunioo  11678  difreicc  11681  iccsplit  11682  uzsplit  11779  fzm1  11787  expcl2lem  12178  expeq0  12196  expnegz  12200  expaddz  12210  expmulz  12212  sqlecan  12274  facdiv  12365  facwordi  12367  bcpasc  12399  resqrex  13084  absexpz  13138  caubnd  13191  summo  13539  zsum  13540  zprod  13744  rpnnen2  13959  ordvdsmul  14022  dvdsprime  14230  prmdvdsexpr  14257  prmfac1  14259  pythagtriplem2  14341  4sqlem11  14473  vdwlem6  14504  vdwlem9  14507  vdwlem13  14511  cshwshashlem3  14582  prmlem0  14591  xpscfv  14959  pleval2  15595  pltletr  15601  plelttr  15602  tsrlemax  15850  f1omvdco2  16473  psgnunilem2  16520  efgredlemc  16763  frgpuptinv  16789  lt6abl  16897  dmdprdsplit2lem  17094  drngmul0or  17417  lvecvs0or  17754  domneq0  17946  baspartn  19455  0top  19485  indistopon  19502  restntr  19683  cnindis  19793  cmpfi  19908  filcon  20384  ufprim  20410  ufildr  20432  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  ovolicc2lem3  21930  rolle  22391  dvivthlem1  22409  coeaddlem  22646  dgrco  22672  plymul0or  22677  aalioulem3  22730  cxpge0  23064  cxpmul2z  23072  cxpcn3lem  23121  scvxcvx  23315  sqf11  23413  ppiublem1  23477  lgsdir2lem2  23599  lgsqrlem2  23617  lmieu  24150  frgraogt3nreg  25120  gxnn0neg  25265  gxnn0suc  25266  nvmul0or  25547  hvmul0or  25942  disjxpin  27447  subfacp1lem4  28627  untsucf  29082  dfon2lem6  29220  dftrpred3g  29316  wfrlem14  29356  wfrlem15  29357  nodenselem4  29444  broutsideof2  29772  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  lineunray  29797  lineelsb2  29798  meran1  29876  ontgval  29896  ordcmp  29912  mblfinlem2  30052  ovoliunnfl  30056  itg2addnclem  30066  finminlem  30136  nn0prpw  30141  refssfne  30176  sdclem2  30235  fdc  30238  divrngidl  30425  fphpdo  30751  pellfundex  30822  jm2.19lem4  30934  jm2.26a  30942  lidldomn1  32727  uzlidlring  32735  bj-sngltag  34541  lkreqN  34895  cvrnbtwn4  35004  4atlem12  35336  elpaddn0  35524  paddasslem17  35560  paddidm  35565  pmapjoin  35576  llnexchb2  35593  dalawlem13  35607  dalawlem14  35608  dochkrshp4  37116  lcfl6  37227
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 185  df-or 370
  Copyright terms: Public domain W3C validator