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

Theorem pm2.61dan 832
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
pm2.61dan.1 ((𝜑𝜓) → 𝜒)
pm2.61dan.2 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Assertion
Ref Expression
pm2.61dan (𝜑𝜒)

Proof of Theorem pm2.61dan
StepHypRef Expression
1 pm2.61dan.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 450 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61dan.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
43ex 450 . 2 (𝜑 → (¬ 𝜓𝜒))
52, 4pm2.61d 170 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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-an 386
This theorem is referenced by:  pm2.61ddan  833  pm2.61dda  834  nfsb4t  2388  pm2.61danel  2910  ifeq1da  4114  ifeq2da  4115  ifeq12da  4116  ifclda  4118  ifeqda  4119  ifbothda  4121  2if2  4134  nelsnOLD  4211  somin1  5527  xpcan  5568  fvmpti  6279  fvmptss  6290  funressn  6423  ovima0  6810  oeoa  7674  oeoe  7676  omabs  7724  eceqoveq  7850  domdifsn  8040  pw2f1olem  8061  mapdom1  8122  marypha1lem  8336  supval2  8358  infdifsn  8551  carden2b  8790  fidomtri  8816  dfac12lem2  8963  cdadom1  9005  infunsdom1  9032  infunsdom  9033  itunisuc  9238  gchdomtri  9448  xrmax2  12004  xrmin1  12005  ifle  12025  xmulneg1  12096  xrsupsslem  12134  xrinfmsslem  12135  fzneuz  12417  seqf1olem1  12835  bccmpl  13091  bcval5  13100  bcpasc  13103  bccl  13104  hasheni  13131  hashfn  13159  hashdom  13163  hashdomi  13164  hashge1  13173  hashbc  13232  sumz  14447  sumss  14449  fsumsplitsn  14468  sumsplit  14493  prod1  14668  prodss  14671  fprodsplitsn  14714  fprodle  14721  bitsmod  15152  sadadd2lem2  15166  sadcaddlem  15173  gcddvds  15219  gcdcl  15222  gcdneg  15237  dvdslcm  15305  lcmcl  15308  lcmneg  15310  lcmgcd  15314  lcmfcl  15335  dvdslcmf  15338  pcgcd  15576  pcmpt  15590  pcmpt2  15591  pcprod  15593  fldivp1  15595  prmreclem4  15617  vdwlem6  15684  ramub1lem1  15724  cidpropd  16364  rescabs  16487  lubval  16978  glbval  16991  joinval  16999  meetval  17013  acsexdimd  17177  gsumpropd2lem  17267  gsumval2  17274  f1otrspeq  17861  pmtrfinv  17875  psgnunilem1  17907  gsumval3  18302  ablfac1c  18464  ablfac1eu  18466  mgpress  18494  psrbas  19372  resspsrbas  19409  mplmonmul  19458  mplcoe1  19459  mplcoe5  19462  opsrle  19469  opsrbaslem  19471  opsrbaslemOLD  19472  psrbaspropd  19599  mplbaspropd  19601  frlmsslsp  20129  mdetdiag  20399  mdetunilem7  20418  mdetunilem9  20420  maducoeval2  20440  madurid  20444  opnnei  20918  restbas  20956  hauspwdom  21298  ptcmplem5  21854  xrsmopn  22609  xrhmeo  22739  lebnum  22757  pcohtpylem  22813  pcoass  22818  pcorevlem  22820  icombl  23326  ioombl  23327  mbfconstlem  23390  mbfima  23393  i1fd  23442  mbfi1fseqlem5  23480  itg2const2  23502  itg2seq  23503  itg2uba  23504  itg2splitlem  23509  itg2split  23510  itg2monolem1  23511  itg2gt0  23521  itg2cnlem1  23522  itg2cnlem2  23523  iblss  23565  iblss2  23566  itgss  23572  bddmulibl  23599  coemullem  24000  aaliou2b  24090  isppw2  24835  mule1  24868  ppip1le  24881  dchrelbas3  24957  dchrpt  24986  bposlem3  25005  bposlem5  25007  bposlem6  25008  lgslem4  25019  lgsneg  25040  lgsmod  25042  lgsdilem  25043  lgsdir  25051  lgsdi  25053  lgsne0  25054  lgsquad3  25106  dchrvmasum2if  25180  midexlem  25581  colperpex  25619  outpasch  25641  hlpasch  25642  lnopp2hpgb  25649  lmieu  25670  inaghl  25725  cgrg3col4  25728  pthdlem1  26656  nmcfnlbi  28895  elpreq  29344  disjdifprg  29372  disjun0  29392  f1ocnt  29544  xrge0npcan  29679  archiabl  29737  orngsqr  29789  psgnfzto1stlem  29835  1smat1  29855  esumcst  30110  esumrnmpt2  30115  hasheuni  30132  esumcvg  30133  ddemeas  30284  omssubadd  30347  eulerpartlemgc  30409  eulerpartlemb  30415  plymulx  30610  signswmnd  30619  signstfvneq0  30634  erdsze2lem1  31170  mrsubvrs  31404  trpredlem1  31711  unblimceq0lem  32481  unbdqndv2lem2  32485  knoppndvlem10  32496  wl-spae  33286  wl-cbvalnaed  33299  wl-nfeqfb  33303  unccur  33372  poimirlem15  33404  poimirlem22  33411  itg2addnclem  33441  itg2addnclem2  33442  iblmulc2nc  33455  ftc1anclem5  33469  ftc1anc  33473  dvasin  33476  areacirclem5  33484  exmid2  33881  3dim1  34579  3dim2  34580  3dim3  34581  3atlem3  34597  3atlem7  34601  lvolnle3at  34694  2lplnja  34731  paddasslem18  34949  lhpexle3lem  35123  4atex  35188  cdlemd5  35315  cdleme16  35398  cdleme20  35438  cdleme21j  35450  cdleme21  35451  cdleme32snaw  35549  cdleme32fvcl  35554  cdleme32le  35561  cdlemeg46gf  35647  cdleme48gfv  35651  cdleme50trn12  35666  cdlemg6  35737  cdlemg7N  35740  cdlemg38  35829  cdlemg46  35849  dibvalrel  36278  dihlss  36365  dihglblem5aN  36407  dihmeetbN  36418  dihmeetALTN  36442  dihatlat  36449  dihatexv  36453  dvh3dim2  36563  dvh3dim3N  36564  lclkrlem2h  36629  mapdh8d  36898  mapdh8g  36901  hdmap11lem2  36960  ttac  37429  pw2f1ocnv  37430  aomclem5  37454  isnumbasgrplem3  37501  iocmbl  37624  radcnvrat  38339  bccbc  38370  binomcxp  38382  fnchoice  39014  fiiuncl  39060  disjxp1  39064  eliin2f  39113  founiiun0  39199  axccdom  39238  axccd2  39252  fzisoeu  39333  fperiodmul  39337  upbdrech2  39341  fzdifsuc2  39344  uzfissfz  39361  supxrgere  39368  supxrgelem  39372  supxrge  39373  suplesup  39374  infrpge  39386  xrlexaddrp  39387  xralrple2  39389  infxr  39402  infleinflem1  39405  infleinflem2  39406  infleinf  39407  xralrple3  39409  fiminre2  39413  xrralrecnnge  39432  uzublem  39476  supxrmnf2  39479  infxrpnf  39493  infxrpnf2  39512  supminfxr  39513  supminfxr2  39518  ioondisj2  39523  iccdifprioo  39551  fmul01lt1lem1  39622  fmul01lt1lem2  39623  limciccioolb  39659  lptioo2  39669  lptioo1  39670  limcicciooub  39675  lptre2pt  39678  limcresiooub  39680  limcresioolb  39681  limcleqr  39682  climfveq  39707  climfveqf  39718  limsupubuzlem  39750  limsupubuz  39751  limsupmnfuzlem  39764  limsupre3uzlem  39773  limsup10exlem  39804  coskpi2  39846  cosknegpi  39849  icccncfext  39869  cncfiooicclem1  39875  cncfiooicc  39876  cncfiooiccre  39877  dvbdfbdioolem2  39913  ioodvbdlimc1lem1  39915  ioodvbdlimc1lem2  39916  ioodvbdlimc2lem  39918  dvnxpaek  39926  dvnprodlem1  39930  dvnprodlem3  39932  volioc  39957  itgioocnicc  39962  iblcncfioo  39963  volico  39969  sublevolico  39970  ismbl3  39972  ovolsplit  39974  volioore  39976  voliooico  39978  voliccico  39985  stoweidlem14  40000  stoweidlem26  40012  stoweidlem28  40014  stoweidlem55  40041  stoweid  40049  stirlinglem5  40064  stirlinglem12  40071  dirkerper  40082  dirkertrigeqlem3  40086  dirkertrigeq  40087  dirkercncflem1  40089  dirkercncflem2  40090  dirkercncf  40093  fourierdlem10  40103  fourierdlem12  40105  fourierdlem24  40117  fourierdlem30  40123  fourierdlem31  40124  fourierdlem32  40125  fourierdlem33  40126  fourierdlem34  40127  fourierdlem35  40128  fourierdlem37  40130  fourierdlem40  40133  fourierdlem41  40134  fourierdlem42  40135  fourierdlem43  40136  fourierdlem44  40137  fourierdlem46  40138  fourierdlem48  40140  fourierdlem49  40141  fourierdlem51  40143  fourierdlem54  40146  fourierdlem62  40154  fourierdlem64  40156  fourierdlem65  40157  fourierdlem70  40162  fourierdlem71  40163  fourierdlem73  40165  fourierdlem74  40166  fourierdlem75  40167  fourierdlem78  40170  fourierdlem79  40171  fourierdlem80  40172  fourierdlem81  40173  fourierdlem82  40174  fourierdlem92  40184  fourierdlem93  40185  fourierdlem97  40189  fourierdlem101  40193  fourierdlem102  40194  fourierdlem103  40195  fourierdlem104  40196  fourierdlem109  40201  fourierdlem114  40206  sqwvfoura  40214  sqwvfourb  40215  fourierswlem  40216  fouriersw  40217  elaa2lem  40219  etransclem15  40235  etransclem19  40239  etransclem20  40240  etransclem22  40242  etransclem23  40243  etransclem24  40244  etransclem25  40245  etransclem27  40247  etransclem28  40248  etransclem35  40255  etransclem38  40258  qndenserrnbl  40284  ioorrnopn  40294  ioorrnopnxrlem  40295  ioorrnopnxr  40296  prsal  40307  salexct  40321  issalnnd  40332  sge0sn  40365  sge0tsms  40366  sge0cl  40367  sge0f1o  40368  sge0sup  40377  sge0less  40378  sge0pr  40380  sge0prle  40387  sge0le  40393  sge0split  40395  sge0splitmpt  40397  sge0iunmptlemfi  40399  sge0iunmpt  40404  sge0isum  40413  sge0xaddlem1  40419  sge0xadd  40421  sge0gtfsumgt  40429  nnfoctbdjlem  40441  iundjiun  40446  meadjun  40448  ismeannd  40453  voliunsge0lem  40458  caragenfiiuncl  40498  omeiunltfirp  40502  carageniuncl  40506  caragenunicl  40507  isomenndlem  40513  isomennd  40514  hoicvr  40531  ovnssle  40544  ovn0  40549  ovnsubadd  40555  hsphoidmvle2  40568  hoidmvval0b  40573  hoidmv1lelem1  40574  hoidmv1lelem2  40575  hoidmv1le  40577  hoidmvlelem2  40579  hoidmvlelem3  40580  hoidmvlelem5  40582  hoidmvle  40583  ovnhoilem1  40584  ovnhoi  40586  ovnlecvr2  40593  hspdifhsp  40599  hoidifhspdmvle  40603  hoiqssbl  40608  hspmbllem1  40609  hspmbllem2  40610  hspmbl  40612  hoimbl  40614  volico2  40624  ovolval2lem  40626  ovnsubadd2lem  40628  ovolval4lem1  40632  ovolval4lem2  40633  ovolval5lem1  40635  vonhoire  40655  iunhoiioo  40659  vonioo  40665  vonicc  40668  vonsn  40674  pimrecltpos  40688  incsmflem  40719  smfpimltxr  40725  smfconst  40727  decsmflem  40743  smfpimgtxr  40757  smfrec  40765  sharhght  40823
  Copyright terms: Public domain W3C validator