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

Theorem jaodan 785
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
jaodan.1
jaodan.2
Assertion
Ref Expression
jaodan

Proof of Theorem jaodan
StepHypRef Expression
1 jaodan.1 . . . 4
21ex 434 . . 3
3 jaodan.2 . . . 4
43ex 434 . . 3
52, 4jaod 380 . 2
65imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  /\wa 369
This theorem is referenced by:  mpjaodan  786  andi  867  ccase  946  mpjao3dan  1295  relop  5158  poltletr  5407  oeoa  7265  oeoe  7267  phplem3  7718  ssnnfi  7759  unwdomg  8031  numwdom  8461  infpssrlem5  8708  fin23lem24  8723  fin23lem28  8741  fin1a2lem10  8810  zornn0g  8906  gchdomtri  9028  fpwwe2lem12  9040  fpwwe2lem13  9041  msqgt0  10098  recextlem2  10205  lemul1a  10421  nnnn0addcl  10851  un0addcl  10854  un0mulcl  10855  elz2  10906  xaddnemnf  11462  xaddnepnf  11463  rexmul  11492  xlemul1a  11509  xrsupsslem  11527  xrinfmsslem  11528  ixxun  11574  fzsplit2  11739  fzsuc2  11766  elfzp12  11786  seqf1olem2  12147  expp1  12173  expneg  12174  expcllem  12177  mulexpz  12206  expaddz  12210  expmulz  12212  faclbnd4lem3  12373  faclbnd4lem4  12374  faclbnd4  12375  bcpasc  12399  wrdsymb0  12575  ccatass  12605  ccatrn  12606  ccatswrd  12681  cats1un  12701  revccat  12740  summo  13539  sumss2  13548  fsumsplit  13562  geomulcvg  13685  fprodsplit  13770  ef0lem  13814  dvdseq  14033  odd2np1  14046  sadcaddlem  14107  gcdcllem3  14151  rpexp1i  14262  pcid  14396  4sqlem16  14478  funcres2c  15270  lubun  15753  mulgneg  16160  mulgnn0z  16162  frgpup3lem  16795  gsumzunsnd  16982  gsumunsnfd  16983  dprddisj2  17087  dprddisj2OLD  17088  dmdprdsplit2  17095  dprdsplit  17097  gsumdixpOLD  17257  gsumdixp  17258  lssvs0or  17756  evlslem4OLD  18173  evlslem4  18174  refun0  20016  txhaus  20148  xkoptsub  20155  ptunhmeo  20309  xpsxmetlem  20882  xpsmet  20885  mbfss  22053  itg1addlem2  22104  iblss2  22212  itgsplit  22242  limcres  22290  ftc1lem5  22441  coe1mul3  22500  dgrlt  22663  abelthlem3  22828  atanlogaddlem  23244  atanlogsub  23247  atans2  23262  efrlim  23299  bposlem2  23560  lgsdir2lem4  23601  2sqb  23653  pntpbnd1  23771  ostthlem1  23812  hlbtwn  23995  brbtwn2  24208  axcontlem2  24268  uvtx01vtx  24492  isoun  27520  nn0sqeq1  27562  mul2lt0bi  27569  eliccelico  27588  elicoelioo  27589  fzsplit3  27599  xrge0iifhom  27919  esumsplit  28063  sibfinima  28281  subfacp1lem4  28627  subfacp1lem5  28628  mclsax  28929  bpoly2  29819  bpoly3  29820  ftc1cnnc  30089  ftc1anclem2  30091  eqfnun  30212  fdc  30238  incsequz2  30242  unichnidl  30428  rexzrexnn0  30737  pell14qrexpcl  30803  elpell1qr2  30808  acongeq  30921  jm2.23  30938  rpnnen3  30974  radcnvrat  31195  dvdslcm  31204  lcmeq0  31206  lcmcl  31207  lcmneg  31209  lcmgcd  31213  sumpair  31410  cncfiooicclem1  31696  fourierdlem80  31969  fourierdlem93  31982  bnj1137  34051  lkrss2N  34894  cdlemg27b  36422  tendoex  36701  dihmeetlem2N  37026  dvh3dim3N  37176
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  df-an 371
  Copyright terms: Public domain W3C validator