MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaoi Structured version   Visualization version   GIF version

Theorem jaoi 875
Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)
Hypotheses
Ref Expression
jaoi.1 (𝜑𝜓)
jaoi.2 (𝜒𝜓)
Assertion
Ref Expression
jaoi ((𝜑𝜒) → 𝜓)

Proof of Theorem jaoi
StepHypRef Expression
1 pm2.53 869 . . 3 ((𝜑𝜒) → (¬ 𝜑𝜒))
2 jaoi.2 . . 3 (𝜒𝜓)
31, 2syl6 35 . 2 ((𝜑𝜒) → (¬ 𝜑𝜓))
4 jaoi.1 . 2 (𝜑𝜓)
53, 4pm2.61d2 173 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 865
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 198  df-or 866
This theorem is referenced by:  jao1i  876  jaod  877  pm1.4  887  pm3.2ni  896  pm1.2  918  pm2.4  921  pm2.41  922  orim12i  923  pm1.5  934  pm2.42  957  jaoa  969  jaoian  970  pm4.44  1010  andi  1021  annotanannotOLD  1025  ecase3  1046  cases2ALT  1062  consensus  1068  jaoi3  1076  1fpid3  1095  19.33  1974  19.33b  1975  nfim1  2233  dfsb2  2534  mooran1  2702  2eu3  2730  eueq3  3590  sbcor  3688  sspss  3915  sspsstr  3921  elun  3963  ssun  4002  inss  4050  ifbi  4311  ifcomnan  4344  elpr2  4405  rabsnifsb  4459  tpprceq3  4536  tppreqb  4537  pwpw0  4545  sssn  4558  snsssn  4571  preq12b  4580  prnebg  4587  preq12nebg  4596  elpr2elpr  4602  pwsnALT  4634  prproe  4639  3elpr2eq  4640  unissint  4704  zfpair  5107  propeqop  5175  propssopi  5176  opthhausdorff  5185  opthhausdorff0  5186  iunopeqop  5189  sotri2  5749  sotri3  5750  somincom  5754  ordssun  6049  onun2i  6065  unizlim  6066  onxpdisj  6069  tpres  6700  sorpssuni  7185  sorpssint  7186  ordeleqon  7227  ordunisuc  7271  orduninsuc  7282  tfinds  7298  limomss  7309  limom  7319  soxp  7533  ressuppssdif  7559  tfr2b  7737  omopthi  7983  domnsym  8334  brwdom  8720  cantnfvalf  8818  djuss  9038  djuunxp  9039  eldju2ndl  9042  eldju2ndr  9043  djuun  9044  updjud  9052  iscard3  9208  cflim2  9379  sornom  9393  isfin5  9415  isfin6  9416  sdom2en01  9418  fin23lem29  9457  fin23lem30  9458  fin56  9509  fin67  9511  hsmexlem9  9541  axcc4dom  9557  axdc3lem2  9567  axdc3lem4  9569  brdom3  9644  winainflem  9809  r1tskina  9898  indpi  10023  ltxrlt  10402  ltlen  10432  elnnnn0b  11622  nn0sub  11628  nn0n0n1ge2b  11644  nn0ge2m1nn  11645  xnn0xr  11653  xnn0nemnf  11659  elnn0z  11675  nn0lt10b  11724  nn0le2is012  11726  nn0ind-raph  11762  znnn0nn  11774  uzin  11957  indstr2  12005  nn0ledivnn  12176  xrnemnf  12186  xrnepnf  12187  mnfltxr  12196  xnn0n0n1ge2b  12200  xnn0ge0  12202  nn0pnfge0OLD  12203  xnn0xaddcl  12303  xnn0lenn0nn0  12312  xnn0xadd0  12314  xmullem2  12332  rexmul  12338  xnn0xrge0  12567  elfzonlteqm1  12787  elfznelfzo  12816  injresinjlem  12831  injresinj  12832  fldiv4p1lem1div2  12879  fldiv4lem1div2  12881  modfzo0difsn  12985  ssnn0fi  13027  fsuppmapnn0fiubex  13034  m1expcl2  13124  m1expeven  13149  sq01  13228  nn0opthi  13296  facp1  13304  faclbnd3  13318  faclbnd4lem1  13319  faclbnd4lem3  13321  bcn1  13339  hashnemnf  13371  hashv01gt1  13372  hashneq0  13392  hashrabrsn  13398  hashrabsn01  13399  hashrabsn1  13400  hashunx  13412  hashsnle1  13441  hashfzp1  13454  hash2pwpr  13494  hashge2el2difr  13499  swrdnd2  13676  repswswrd  13774  scshwfzeqfzo  13815  relexpsucr  14011  relexpsucl  14015  relexpcnv  14017  relexprelg  14020  relexpdmg  14024  relexprng  14028  relexpfld  14031  relexpaddg  14035  sumz  14695  arisum  14833  arisum2  14834  ntrivcvg  14869  prod1  14914  fprodfac  14943  mod2eq1n2dvds  15310  mulsucdiv2z  15316  nn0o1gt2  15336  nno  15337  nn0o  15338  sumeven  15349  sumodd  15350  divalglem1  15356  divalglem6  15360  gcdaddmlem  15483  dfgcd2  15501  mulgcd  15503  lcmf  15584  lcmfunsnlem2lem2  15590  lcmfunsnlem2  15591  prm2orodd  15641  dfphi2  15715  nnnn0modprm0  15747  prm23lt5  15755  oddprmdvds  15843  4sqlem19  15903  ramz  15965  prmolefac  15986  prmgaplem7  15997  cshwshashlem1  16033  ressval3d  16167  ressval3dOLD  16168  firest  16317  xpsfeq  16448  xpsfrnel2  16449  funcres2c  16784  symgfix2  18056  pmtrprfval  18127  m1expaddsub  18138  psgnprfval  18161  gsumzunsnd  18575  sralem  19405  0ringnnzr  19497  prmirred  20070  frgpcyg  20148  cnmsgnsubg  20149  psgninv  20154  zrhpsgnelbas  20167  m2detleiblem1  20661  symgmatr01lem  20691  pmatcollpw3fi1  20826  indiscld  21129  pnfnei  21258  mnfnei  21259  alexsubALTlem2  22085  alexsubALTlem3  22086  dscmet  22610  xrtgioo  22842  ishl2  23399  iunmbl2  23560  icombl  23567  ioombl  23568  recnprss  23904  recnperf  23905  dvexp2  23953  dvexp3  23977  dvne0f1  24011  plypf1  24204  taylfvallem1  24347  taylfval  24349  tayl0  24352  coseq0negpitopi  24492  logfac  24583  cxpexp  24650  pythag  24783  reasinsin  24859  harmonicbnd3  24970  lgslem4  25261  gausslemma2dlem0i  25325  lgsquadlem2  25342  2lgslem3  25365  2lgs  25368  2lgsoddprmlem3  25375  cchhllem  26003  lfgrnloop  26256  uhgr2edg  26337  usgredg4  26346  usgredg2v  26356  usgrexmplef  26389  nb3grprlem1  26520  uvtx01vtx  26540  uvtxa01vtx0OLD  26542  wlk1walk  26785  upgriswlk  26787  pthdadjvtx  26876  upgrwlkdvdelem  26882  pthdlem2lem  26913  2pthon3v  27105  clwwlknclwwlkdifsOLD  27144  clwwlkn  27193  clwwlkneq0  27198  eupth2lem3lem4  27426  konigsberg  27452  3vfriswmgrlem  27474  1to2vfriswmgr  27476  1to3vfriswmgr  27477  frgrregorufr0  27521  numclwlk1  27573  ex-pr  27640  shunssi  28577  cvmdi  29533  1neg1t1neg1  29863  iundisj2cnt  29907  fz1nnct  29909  xrge0iifiso  30328  esumpr2  30476  measiuns  30627  sxbrsigalem0  30680  bnj964  31357  subfacval3  31515  kur14lem7  31538  mrsubcv  31751  nepss  31942  fz0n  31959  bccolsum  31968  dfon2lem7  32035  trpredlem1  32068  trpred0  32077  sltres  32157  nolesgn2o  32166  nosep1o  32174  altopthsn  32410  elhf2  32624  nn0prpw  32660  dissym1  32758  ordcmp  32784  bj-jaoi1  32891  bj-jaoi2  32892  bj-andnotim  32909  bj-sbsb  33155  finxpreclem2  33561  wl-equsal1i  33661  tan2h  33732  poimirlem23  33763  poimirlem32  33772  itg2addnclem  33791  orfa1  34215  orfa2  34216  inex3  34439  inxpex  34440  elpadd0  35607  hbtlem5  38216  rp-fakeimass  38374  rp-isfinite6  38381  iunrelexp0  38511  relexpss1d  38514  relexpmulg  38519  iunrelexpmin2  38521  relexp01min  38522  relexp0a  38525  relexpxpmin  38526  relexpaddss  38527  clsk1indlem3  38858  ssrecnpr  39024  seff  39025  sblpnf  39026  expgrowthi  39049  dvconstbi  39050  19.33-2  39098  ax6e2ndeq  39290  en3lpVD  39591  undif3VD  39629  ax6e2ndeqVD  39656  ax6e2ndeqALT  39678  iooinlbub  40224  raaan2  41666  elprneb  41670  2reu3  41717  afvpcfv0  41752  afvfv0bi  41758  afvco2  41782  afv2orxorb  41834  afv2ndeffv0  41866  afv2fv0b  41872  fvmptrabdm  41900  iccpartltu  41953  iccpartgtl  41954  iccpartgt  41955  iccpartleu  41956  iccpartgel  41957  iccpartnel  41966  odz2prm2pw  42067  fmtnofac1  42074  fmtno4prmfac  42076  pwdif  42093  31prm  42104  lighneallem2  42115  lighneallem3  42116  lighneallem4b  42118  lighneallem4  42119  zeo2ALTV  42174  nn0o1gt2ALTV  42197  nn0oALTV  42199  stgoldbwt  42256  sbgoldbwt  42257  sbgoldbalt  42261  sbgoldbm  42264  sbgoldbo  42267  nnsum3primesle9  42274  nnsum4primeseven  42280  nnsum4primesevenALTV  42281  wtgoldbnnsum4prm  42282  bgoldbnnsum3prm  42284  bgoldbtbndlem1  42285  bgoldbtbnd  42289  tgoldbach  42297  upgrwlkupwlk  42306  elsprel  42310  prsprel  42322  sprsymrelfolem2  42328  ztprmneprm  42710  gsumpr  42724  islinindfis  42823  lindslinindsimp2lem5  42836  lindslinindsimp2  42837  lindsrng01  42842  elfzolborelfzop1  42894  flnn0div2ge  42912  blennn0elnn  42956  blen1b  42967  nnolog2flm1  42969  blengt1fldiv2p1  42972  0dig2pr01  42989  dignn0flhalf  42997  nn0sumshdiglemB  42999  nn0sumshdiglem1  43000
  Copyright terms: Public domain W3C validator