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

Theorem jaoi 393
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 387 . . 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 382
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 384
This theorem is referenced by:  jaod  394  pm1.4  400  jaoa  531  pm1.2  534  orim12i  537  pm1.5  543  pm2.41  596  pm2.42  597  pm2.4  598  pm4.44  600  jaoian  841  jao1i  842  pm3.2ni  917  andi  929  annotanannotOLD  960  ecase3  1001  cases2ALT  1017  consensus  1023  jaoi3  1031  1fpid3  1049  19.33  1852  19.33b  1853  nfim1  2105  dfsb2  2401  mooran1  2556  2eu3  2584  eueq3  3414  sbcor  3512  sspss  3739  sspsstr  3745  elun  3786  ssun  3825  inss  3875  undif3OLD  3922  ifbi  4140  ifcomnan  4170  elpr2  4232  elpr2OLD  4233  eqoreldifOLD  4258  rabsnifsb  4289  tpprceq3  4367  tppreqb  4368  pwpw0  4376  sssn  4390  snsssn  4404  preq12b  4413  prnebg  4420  elpr2elpr  4429  pwsnALT  4461  prproe  4466  3elpr2eq  4467  unissint  4533  zfpair  4934  propeqop  4999  propssopi  5000  iunopeqop  5010  sotri2  5560  sotri3  5561  somincom  5565  ordelinelOLD  5864  ordssun  5865  onun2i  5881  unizlim  5882  onxpdisj  5885  funtpgOLD  5981  fvfundmfvn0  6264  tpres  6507  sorpssuni  6988  sorpssint  6989  ordeleqon  7030  ordunisuc  7074  orduninsuc  7085  tfinds  7101  limomss  7112  limom  7122  soxp  7335  ressuppssdif  7361  tfr2b  7537  omopthi  7782  domnsym  8127  brwdom  8513  cantnfvalf  8600  iscard3  8954  cflim2  9123  sornom  9137  isfin5  9159  isfin6  9160  sdom2en01  9162  fin23lem29  9201  fin23lem30  9202  fin56  9253  fin67  9255  hsmexlem9  9285  axcc4dom  9301  axdc3lem2  9311  axdc3lem4  9313  brdom3  9388  winainflem  9553  r1tskina  9642  indpi  9767  ltxrlt  10146  ltlen  10176  elnnnn0b  11375  nn0sub  11381  nn0n0n1ge2b  11397  nn0ge2m1nn  11398  xnn0xr  11406  xnn0nemnf  11412  elnn0z  11428  nn0lt10b  11477  nn0le2is012  11479  nn0ind-raph  11515  znnn0nn  11527  uzin  11758  indstr2  11805  nn0ledivnn  11979  xrnemnf  11989  xrnepnf  11990  mnfltxr  11999  xnn0n0n1ge2b  12003  xnn0ge0  12005  nn0pnfge0OLD  12006  xnn0xaddcl  12104  xnn0lenn0nn0  12113  xnn0xadd0  12115  xmullem2  12133  rexmul  12139  xnn0xrge0  12363  elfzonlteqm1  12583  elfznelfzo  12613  injresinjlem  12628  injresinj  12629  fldiv4p1lem1div2  12676  fldiv4lem1div2  12678  modfzo0difsn  12782  ssnn0fi  12824  fsuppmapnn0fiubex  12832  m1expcl2  12922  m1expeven  12947  sq01  13026  nn0opthi  13097  facp1  13105  faclbnd3  13119  faclbnd4lem1  13120  faclbnd4lem3  13122  bcn1  13140  hashnemnf  13172  hashv01gt1  13173  hashneq0  13193  hashrabrsn  13199  hashrabsn01  13200  hashrabsn1  13201  hashunx  13213  hashsnle1  13243  hashfzp1  13256  hash2pwpr  13296  hashge2el2difr  13301  swrdnd2  13479  repswswrd  13577  scshwfzeqfzo  13618  relexpsucr  13813  relexpsucl  13817  relexpcnv  13819  relexprelg  13822  relexpdmg  13826  relexprng  13830  relexpfld  13833  relexpaddg  13837  sumz  14497  arisum  14636  arisum2  14637  ntrivcvg  14673  prod1  14718  fprodfac  14747  mod2eq1n2dvds  15118  mulsucdiv2z  15124  nn0o1gt2  15144  nno  15145  nn0o  15146  sumeven  15157  sumodd  15158  divalglem1  15164  divalglem6  15168  gcdaddmlem  15292  dfgcd2  15310  mulgcd  15312  lcmf  15393  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  prm2orodd  15451  dfphi2  15526  nnnn0modprm0  15558  prm23lt5  15566  oddprmdvds  15654  4sqlem19  15714  ramz  15776  prmolefac  15797  prmgaplem7  15808  cshwshashlem1  15849  ressval3d  15984  firest  16140  xpsfeq  16271  xpsfrnel2  16272  funcres2c  16608  symgfix2  17882  pmtrprfval  17953  m1expaddsub  17964  psgnprfval  17987  gsumzunsnd  18401  sralem  19225  0ringnnzr  19317  prmirred  19891  frgpcyg  19970  cnmsgnsubg  19971  psgninv  19976  zrhpsgnelbas  19988  m2detleiblem1  20478  symgmatr01lem  20507  pmatcollpw3fi1  20641  indiscld  20943  pnfnei  21072  mnfnei  21073  alexsubALTlem2  21899  alexsubALTlem3  21900  dscmet  22424  xrtgioo  22656  ishl2  23212  iunmbl2  23371  icombl  23378  ioombl  23379  recnprss  23713  recnperf  23714  dvexp2  23762  dvexp3  23786  dvne0f1  23820  plypf1  24013  taylfvallem1  24156  taylfval  24158  tayl0  24161  coseq0negpitopi  24300  logfac  24392  cxpexp  24459  pythag  24592  reasinsin  24668  harmonicbnd3  24779  lgslem4  25070  gausslemma2dlem0i  25134  lgsquadlem2  25151  2lgslem3  25174  2lgs  25177  2lgsoddprmlem3  25184  cchhllem  25812  lfgrnloop  26065  uhgr2edg  26145  usgredg4  26154  usgredg2v  26164  usgrexmplef  26196  nb3grprlem1  26326  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  wlk1walk  26591  upgriswlk  26593  pthdadjvtx  26682  upgrwlkdvdelem  26688  pthdlem2lem  26719  2pthon3v  26908  clwwlknclwwlkdifsOLD  26947  clwwlkn  26985  clwwlkneq0  26990  eupth2lem3lem4  27209  konigsberg  27235  3vfriswmgrlem  27257  1to2vfriswmgr  27259  1to3vfriswmgr  27260  frgrregorufr0  27304  ex-pr  27417  shunssi  28355  cvmdi  29311  1neg1t1neg1  29642  iundisj2cnt  29686  fz1nnct  29688  xrge0iifiso  30109  esumpr2  30257  measiuns  30408  sxbrsigalem0  30461  bnj964  31139  subfacval3  31297  kur14lem7  31320  mrsubcv  31533  nepss  31725  fz0n  31742  bccolsum  31751  dfon2lem7  31818  trpredlem1  31851  trpred0  31860  sltres  31940  nolesgn2o  31949  nosep1o  31957  altopthsn  32193  elhf2  32407  nn0prpw  32443  dissym1  32545  ordcmp  32571  bj-jaoi1  32681  bj-jaoi2  32682  bj-andnotim  32698  bj-sbsb  32949  finxpreclem2  33357  wl-equsal1i  33459  tan2h  33531  poimirlem23  33562  poimirlem32  33571  itg2addnclem  33591  orfa1  34016  orfa2  34017  inex3  34247  inxpex  34248  elpadd0  35413  hbtlem5  38015  rp-fakeimass  38174  rp-isfinite6  38181  iunrelexp0  38311  relexpss1d  38314  relexpmulg  38319  iunrelexpmin2  38321  relexp01min  38322  relexp0a  38325  relexpxpmin  38326  relexpaddss  38327  clsk1indlem3  38658  ssrecnpr  38824  seff  38825  sblpnf  38826  expgrowthi  38849  dvconstbi  38850  19.33-2  38898  ax6e2ndeq  39092  en3lpVD  39394  undif3VD  39432  ax6e2ndeqVD  39459  ax6e2ndeqALT  39481  iooinlbub  40041  raaan2  41496  2reu3  41509  afvpcfv0  41547  afvfv0bi  41553  afvco2  41577  elprneb  41620  fvmptrabdm  41632  iccpartltu  41686  iccpartgtl  41687  iccpartgt  41688  iccpartleu  41689  iccpartgel  41690  iccpartnel  41699  odz2prm2pw  41800  fmtnofac1  41807  fmtno4prmfac  41809  pwdif  41826  31prm  41837  lighneallem2  41848  lighneallem3  41849  lighneallem4b  41851  lighneallem4  41852  zeo2ALTV  41907  nn0o1gt2ALTV  41930  nn0oALTV  41932  stgoldbwt  41989  sbgoldbwt  41990  sbgoldbalt  41994  sbgoldbm  41997  sbgoldbo  42000  nnsum3primesle9  42007  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem1  42018  bgoldbtbnd  42022  tgoldbach  42030  tgoldbachOLD  42037  upgrwlkupwlk  42046  elsprel  42050  prsprel  42062  sprsymrelfolem2  42068  ztprmneprm  42450  gsumpr  42464  islinindfis  42563  lindslinindsimp2lem5  42576  lindslinindsimp2  42577  lindsrng01  42582  elfzolborelfzop1  42634  flnn0div2ge  42652  blennn0elnn  42696  blen1b  42707  nnolog2flm1  42709  blengt1fldiv2p1  42712  0dig2pr01  42729  dignn0flhalf  42737  nn0sumshdiglemB  42739  nn0sumshdiglem1  42740
  Copyright terms: Public domain W3C validator