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

Theorem jaoi 394
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 388 . . 3 ((𝜑𝜒) → (¬ 𝜑𝜒))
2 jaoi.2 . . 3 (𝜒𝜓)
31, 2syl6 35 . 2 ((𝜑𝜒) → (¬ 𝜑𝜓))
4 jaoi.1 . 2 (𝜑𝜓)
53, 4pm2.61d2 172 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383
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 197  df-or 385
This theorem is referenced by:  jaod  395  pm1.4  401  jaoa  532  pm1.2  535  orim12i  538  pm1.5  544  pm2.41  596  pm2.42  597  pm2.4  598  pm4.44  600  jaoian  823  jao1i  824  pm3.2ni  898  andi  910  ecase3  981  cases2  992  consensus  998  jaoi3  1010  1fpid3  1028  19.33  1810  19.33b  1811  nfim1  2065  dfsb2  2371  mooran1  2525  2eu3  2553  eueq3  3375  sbcor  3473  sspss  3698  sspsstr  3704  elun  3745  ssun  3784  inss  3834  undif3OLD  3881  ifbi  4098  ifcomnan  4128  elpr2  4190  elpr2OLD  4191  eqoreldifOLD  4217  rabsnifsb  4248  tpprceq3  4326  tppreqb  4327  pwpw0  4335  sssn  4349  snsssn  4363  preq12b  4373  prnebg  4380  elpr2elpr  4389  pwsnALT  4420  prproe  4425  3elpr2eq  4426  unissint  4492  zfpair  4895  propeqop  4960  propssopi  4961  iunopeqop  4971  sotri2  5513  sotri3  5514  somincom  5518  ordelinelOLD  5814  ordssun  5815  onun2i  5831  unizlim  5832  onxpdisj  5835  funtpgOLD  5931  fvfundmfvn0  6213  tpres  6451  sorpssuni  6931  sorpssint  6932  ordeleqon  6973  ordunisuc  7017  orduninsuc  7028  tfinds  7044  limomss  7055  limom  7065  soxp  7275  ressuppssdif  7301  tfr2b  7477  omopthi  7722  domnsym  8071  brwdom  8457  cantnfvalf  8547  iscard3  8901  cflim2  9070  sornom  9084  isfin5  9106  isfin6  9107  sdom2en01  9109  fin23lem29  9148  fin23lem30  9149  fin56  9200  fin67  9202  hsmexlem9  9232  axcc4dom  9248  axdc3lem2  9258  axdc3lem4  9260  brdom3  9335  winainflem  9500  r1tskina  9589  indpi  9714  ltxrlt  10093  ltlen  10123  elnnnn0b  11322  nn0sub  11328  nn0n0n1ge2b  11344  nn0ge2m1nn  11345  xnn0xr  11353  xnn0nemnf  11359  elnn0z  11375  nn0lt10b  11424  nn0le2is012  11426  nn0ind-raph  11462  znnn0nn  11474  uzin  11705  indstr2  11752  nn0ledivnn  11926  xrnemnf  11936  xrnepnf  11937  mnfltxr  11946  xnn0n0n1ge2b  11950  xnn0ge0  11952  nn0pnfge0OLD  11953  xnn0xaddcl  12051  xnn0lenn0nn0  12060  xnn0xadd0  12062  xmullem2  12080  rexmul  12086  xnn0xrge0  12310  elfzonlteqm1  12527  elfznelfzo  12557  injresinjlem  12571  injresinj  12572  fldiv4p1lem1div2  12619  fldiv4lem1div2  12621  modfzo0difsn  12725  ssnn0fi  12767  fsuppmapnn0fiubex  12775  m1expcl2  12865  m1expeven  12890  sq01  12969  nn0opthi  13040  facp1  13048  faclbnd3  13062  faclbnd4lem1  13063  faclbnd4lem3  13065  bcn1  13083  hashnemnf  13115  hashv01gt1  13116  hashneq0  13138  hashrabrsn  13144  hashrabsn01  13145  hashrabsn1  13146  hashunx  13158  hashsnle1  13188  hashfzp1  13201  hash2pwpr  13241  hashge2el2difr  13246  swrdnd2  13415  repswswrd  13512  scshwfzeqfzo  13553  relexpsucr  13750  relexpsucl  13754  relexpcnv  13756  relexprelg  13759  relexpdmg  13763  relexprng  13767  relexpfld  13770  relexpaddg  13774  sumz  14434  arisum  14573  arisum2  14574  ntrivcvg  14610  prod1  14655  fprodfac  14684  mod2eq1n2dvds  15052  mulsucdiv2z  15058  nn0o1gt2  15078  nno  15079  nn0o  15080  sumeven  15091  sumodd  15092  divalglem1  15098  divalglem6  15102  gcdaddmlem  15226  dfgcd2  15244  mulgcd  15246  lcmf  15327  lcmfunsnlem2lem2  15333  lcmfunsnlem2  15334  prm2orodd  15385  dfphi2  15460  nnnn0modprm0  15492  prm23lt5  15500  oddprmdvds  15588  4sqlem19  15648  ramz  15710  prmolefac  15731  prmgaplem7  15742  cshwshashlem1  15783  ressval3d  15918  firest  16074  xpsfeq  16205  xpsfrnel2  16206  funcres2c  16542  symgfix2  17817  pmtrprfval  17888  m1expaddsub  17899  psgnprfval  17922  gsumzunsnd  18336  sralem  19158  0ringnnzr  19250  prmirred  19824  frgpcyg  19903  cnmsgnsubg  19904  psgninv  19909  zrhpsgnelbas  19921  m2detleiblem1  20411  symgmatr01lem  20440  pmatcollpw3fi1  20574  indiscld  20876  pnfnei  21005  mnfnei  21006  alexsubALTlem2  21833  alexsubALTlem3  21834  dscmet  22358  xrtgioo  22590  ishl2  23147  iunmbl2  23306  icombl  23313  ioombl  23314  recnprss  23649  recnperf  23650  dvexp2  23698  dvexp3  23722  dvne0f1  23756  plypf1  23949  taylfvallem1  24092  taylfval  24094  tayl0  24097  coseq0negpitopi  24236  logfac  24328  cxpexp  24395  pythag  24528  reasinsin  24604  harmonicbnd3  24715  lgslem4  25006  gausslemma2dlem0i  25070  lgsquadlem2  25087  2lgslem3  25110  2lgs  25113  2lgsoddprmlem3  25120  cchhllem  25748  lfgrnloop  26001  uhgr2edg  26081  usgredg4  26090  usgredg2v  26100  usgrexmplef  26132  nb3grprlem1  26263  uvtxa01vtx0  26278  wlk1walk  26516  upgriswlk  26518  pthdadjvtx  26607  upgrwlkdvdelem  26613  pthdlem2lem  26644  2pthon3v  26820  clwwlknclwwlkdifs  26854  eupth2lem3lem4  27071  konigsberg  27099  3vfriswmgrlem  27121  1to2vfriswmgr  27123  1to3vfriswmgr  27124  frgrregorufr0  27162  numclwwlkffin0  27187  ex-pr  27257  shunssi  28197  cvmdi  29153  1neg1t1neg1  29488  iundisj2cnt  29532  fz1nnct  29534  xrge0iifiso  29955  esumpr2  30103  measiuns  30254  sxbrsigalem0  30307  bnj964  30987  subfacval3  31145  kur14lem7  31168  mrsubcv  31381  nepss  31574  fz0n  31591  bccolsum  31600  dfon2lem7  31668  trpredlem1  31701  trpred0  31710  sltres  31789  nolesgn2o  31798  nosep1o  31806  altopthsn  32043  elhf2  32257  nn0prpw  32293  dissym1  32395  ordcmp  32421  bj-jaoi1  32531  bj-jaoi2  32532  bj-andnotim  32548  bj-sbsb  32799  finxpreclem2  33198  wl-equsal1i  33300  tan2h  33372  poimirlem23  33403  poimirlem32  33412  itg2addnclem  33432  orfa1  33857  orfa2  33858  elpadd0  34914  hbtlem5  37517  rp-fakeimass  37676  rp-isfinite6  37683  iunrelexp0  37813  relexpss1d  37816  relexpmulg  37821  iunrelexpmin2  37823  relexp01min  37824  relexp0a  37827  relexpxpmin  37828  relexpaddss  37829  clsk1indlem3  38161  ssrecnpr  38327  seff  38328  sblpnf  38329  expgrowthi  38352  dvconstbi  38353  19.33-2  38401  ax6e2ndeq  38595  en3lpVD  38900  undif3VD  38938  ax6e2ndeqVD  38965  ax6e2ndeqALT  38987  iooinlbub  39526  raaan2  40938  2reu3  40951  afvpcfv0  40989  afvfv0bi  40995  afvco2  41019  elprneb  41059  iccpartltu  41125  iccpartgtl  41126  iccpartgt  41127  iccpartleu  41128  iccpartgel  41129  iccpartnel  41138  odz2prm2pw  41240  fmtnofac1  41247  fmtno4prmfac  41249  pwdif  41266  31prm  41277  lighneallem2  41288  lighneallem3  41289  lighneallem4b  41291  lighneallem4  41292  zeo2ALTV  41347  nn0o1gt2ALTV  41370  nn0oALTV  41372  stgoldbwt  41429  sbgoldbwt  41430  sbgoldbalt  41434  sbgoldbm  41437  sbgoldbo  41440  nnsum3primesle9  41447  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  bgoldbtbndlem1  41458  bgoldbtbnd  41462  tgoldbach  41470  tgoldbachOLD  41477  upgrwlkupwlk  41486  elsprel  41490  prsprel  41502  sprsymrelfolem2  41508  ztprmneprm  41890  gsumpr  41904  islinindfis  42003  lindslinindsimp2lem5  42016  lindslinindsimp2  42017  lindsrng01  42022  elfzolborelfzop1  42074  flnn0div2ge  42092  blennn0elnn  42136  blen1b  42147  nnolog2flm1  42149  blengt1fldiv2p1  42152  0dig2pr01  42169  dignn0flhalf  42177  nn0sumshdiglemB  42179  nn0sumshdiglem1  42180
  Copyright terms: Public domain W3C validator