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 809
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 413 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61dan.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
43ex 413 . 2 (𝜑 → (¬ 𝜓𝜒))
52, 4pm2.61d 180 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  pm2.61ddan  810  pm2.61dda  811  nfsb4t  2536  sbal2  2570  sbal2OLD  2571  nfsb4tALT  2601  pm2.61danel  3138  ifeq1da  4496  ifeq2da  4497  ifeq12da  4498  ifclda  4500  ifeqda  4501  ifbothda  4503  2if2  4519  somin1  5988  xpcan  6028  fvmpti  6762  fvmptss  6774  funressn  6915  ovima0  7317  oeoa  8214  oeoe  8216  omabs  8265  eceqoveq  8393  domdifsn  8590  pw2f1olem  8611  mapdom1  8672  marypha1lem  8887  supval2  8909  infdifsn  9110  carden2b  9386  fidomtri  9412  dfac12lem2  9560  infunsdom1  9625  infunsdom  9626  itunisuc  9831  gchdomtri  10041  xrmax2  12560  xrmin1  12561  ifle  12581  xnn0lem1lt  12628  xmulneg1  12653  xrsupsslem  12691  xrinfmsslem  12692  fzneuz  12979  seqf1olem1  13400  bccmpl  13660  bcval5  13669  bcpasc  13672  bccl  13673  hasheni  13699  hashfn  13727  hashdom  13731  hashdomi  13732  hashge1  13741  hashbc  13802  pfxval0  14029  sumz  15070  sumss  15072  fsumsplitsn  15091  sumsplit  15114  prod1  15289  prodss  15292  fprodsplitsn  15334  fprodle  15341  bitsmod  15776  sadadd2lem2  15790  sadcaddlem  15797  gcddvds  15843  gcdcl  15846  gcdneg  15861  dvdslcm  15933  lcmcl  15936  lcmneg  15938  lcmgcd  15942  lcmfcl  15963  dvdslcmf  15966  pcgcd  16205  pcmpt  16219  pcmpt2  16220  pcprod  16222  fldivp1  16224  prmreclem4  16246  vdwlem6  16313  ramub1lem1  16353  cidpropd  16971  rescabs  17094  lubval  17585  glbval  17598  joinval  17606  meetval  17620  acsexdimd  17784  gsumpropd2lem  17880  gsumval2  17887  mulgfval  18167  f1otrspeq  18507  pmtrfinv  18521  psgnunilem1  18553  gsumval3  18959  ablfac1c  19125  ablfac1eu  19127  mgpress  19182  psrbas  20089  resspsrbas  20126  mplmonmul  20176  mplcoe1  20177  mplcoe5  20180  opsrle  20187  opsrbaslem  20189  psrbaspropd  20334  mplbaspropd  20336  frlmsslsp  20871  mdetdiag  21139  mdetunilem7  21158  mdetunilem9  21160  maducoeval2  21180  madurid  21184  opnnei  21659  restbas  21697  hauspwdom  22040  ptcmplem5  22595  xrsmopn  23350  xrhmeo  23480  lebnum  23498  pcoass  23558  pcorevlem  23560  icombl  24095  ioombl  24096  mbfconstlem  24158  mbfima  24161  i1fd  24212  mbfi1fseqlem5  24250  itg2const2  24272  itg2seq  24273  itg2uba  24274  itg2splitlem  24279  itg2split  24280  itg2monolem1  24281  itg2gt0  24291  itg2cnlem1  24292  itg2cnlem2  24293  iblss  24335  iblss2  24336  itgss  24342  bddmulibl  24369  coemullem  24770  aaliou2b  24860  isppw2  25621  mule1  25654  ppip1le  25667  dchrelbas3  25743  dchrpt  25772  bposlem3  25791  bposlem5  25793  bposlem6  25794  lgslem4  25805  lgsneg  25826  lgsmod  25828  lgsdilem  25829  lgsdir  25837  lgsdi  25839  lgsne0  25840  lgsquad3  25892  dchrvmasum2if  26002  midexlem  26407  colperpex  26448  outpasch  26470  hlpasch  26471  lnopp2hpgb  26478  lmieu  26499  inaghl  26560  cgrg3col4  26568  pthdlem1  27476  nmcfnlbi  29758  elpreq  30219  disjdifprg  30255  disjun0  30275  f1ocnt  30453  xrge0npcan  30610  psgnfzto1stlem  30671  cyc3genpmlem  30722  cyc3conja  30728  archiabl  30756  orngsqr  30806  1smat1  30970  esumcst  31223  esumrnmpt2  31228  hasheuni  31245  esumcvg  31246  ddemeas  31396  omssubadd  31459  eulerpartlemgc  31521  eulerpartlemb  31527  plymulx  31719  signswmnd  31728  pthhashvtx  32273  erdsze2lem1  32349  mrsubvrs  32668  trpredlem1  32965  unblimceq0lem  33744  unbdqndv2lem2  33748  knoppndvlem10  33759  wl-spae  34645  wl-cbvalnaed  34655  wl-nfeqfb  34659  unccur  34758  poimirlem15  34790  poimirlem22  34797  itg2addnclem  34826  itg2addnclem2  34827  iblmulc2nc  34840  ftc1anclem5  34854  ftc1anc  34858  dvasin  34861  areacirclem5  34869  exmid2  35261  3dim1  36486  3dim2  36487  3dim3  36488  3atlem3  36504  3atlem7  36508  lvolnle3at  36601  2lplnja  36638  paddasslem18  36856  lhpexle3lem  37030  4atex  37095  cdlemd5  37221  cdleme16  37304  cdleme20  37343  cdleme21j  37355  cdleme21  37356  cdleme32snaw  37454  cdleme32fvcl  37459  cdleme32le  37466  cdlemeg46gf  37552  cdleme48gfv  37556  cdleme50trn12  37571  cdlemg6  37642  cdlemg7N  37645  cdlemg38  37734  cdlemg46  37754  dibvalrel  38182  dihlss  38269  dihglblem5aN  38311  dihmeetbN  38322  dihmeetALTN  38346  dihatlat  38353  dihatexv  38357  dvh3dim2  38467  dvh3dim3N  38468  lclkrlem2h  38533  mapdh8d  38802  mapdh8g  38804  hdmap11lem2  38861  dffltz  39152  ttac  39514  pw2f1ocnv  39515  aomclem5  39539  isnumbasgrplem3  39586  iocmbl  39700  r1rankcld  40448  grur1cld  40449  grucollcld  40477  mnuprd  40493  radcnvrat  40527  bccbc  40558  binomcxp  40570  fnchoice  41167  fiiuncl  41208  eliin2f  41252  founiiun0  41332  axccdom  41368  axccd2  41377  fzisoeu  41448  fperiodmul  41452  upbdrech2  41456  fzdifsuc2  41458  uzfissfz  41475  supxrgere  41482  supxrgelem  41486  supxrge  41487  suplesup  41488  infrpge  41500  xrlexaddrp  41501  xralrple2  41503  infxr  41516  infleinflem1  41519  infleinflem2  41520  infleinf  41521  xralrple3  41523  fiminre2  41527  xrralrecnnge  41543  uzublem  41585  supxrmnf2  41588  infxrpnf  41602  infxrpnf2  41620  supminfxr  41621  supminfxr2  41626  ioondisj2  41648  iccdifprioo  41673  fmul01lt1lem1  41746  fmul01lt1lem2  41747  limciccioolb  41783  lptioo2  41793  lptioo1  41794  limcicciooub  41799  lptre2pt  41802  limcresiooub  41804  limcresioolb  41805  limcleqr  41806  climfveq  41831  climfveqf  41842  limsupubuzlem  41874  limsupubuz  41875  limsupmnfuzlem  41888  limsupre3uzlem  41897  climxrre  41912  limsup10exlem  41934  cnrefiisplem  41991  climxlim2lem  42007  dfxlim2v  42009  xlimliminflimsup  42024  coskpi2  42028  cosknegpi  42031  icccncfext  42051  cncfiooicclem1  42057  cncfiooicc  42058  cncfiooiccre  42059  dvbdfbdioolem2  42095  ioodvbdlimc1lem1  42097  ioodvbdlimc1lem2  42098  ioodvbdlimc2lem  42100  dvnxpaek  42108  dvnprodlem1  42112  dvnprodlem3  42114  volioc  42138  itgioocnicc  42143  iblcncfioo  42144  volico  42150  sublevolico  42151  ismbl3  42153  ovolsplit  42155  volioore  42157  voliooico  42159  voliccico  42166  stoweidlem14  42181  stoweidlem26  42193  stoweidlem28  42195  stoweidlem55  42222  stoweid  42230  stirlinglem5  42245  stirlinglem12  42252  dirkerper  42263  dirkertrigeqlem3  42267  dirkertrigeq  42268  dirkercncflem1  42270  dirkercncflem2  42271  dirkercncf  42274  fourierdlem10  42284  fourierdlem12  42286  fourierdlem24  42298  fourierdlem30  42304  fourierdlem31  42305  fourierdlem32  42306  fourierdlem33  42307  fourierdlem34  42308  fourierdlem35  42309  fourierdlem37  42311  fourierdlem40  42314  fourierdlem41  42315  fourierdlem42  42316  fourierdlem43  42317  fourierdlem44  42318  fourierdlem46  42319  fourierdlem48  42321  fourierdlem49  42322  fourierdlem51  42324  fourierdlem54  42327  fourierdlem62  42335  fourierdlem64  42337  fourierdlem65  42338  fourierdlem70  42343  fourierdlem71  42344  fourierdlem73  42346  fourierdlem74  42347  fourierdlem75  42348  fourierdlem78  42351  fourierdlem79  42352  fourierdlem80  42353  fourierdlem81  42354  fourierdlem82  42355  fourierdlem92  42365  fourierdlem93  42366  fourierdlem97  42370  fourierdlem101  42374  fourierdlem102  42375  fourierdlem103  42376  fourierdlem104  42377  fourierdlem109  42382  fourierdlem114  42387  sqwvfoura  42395  sqwvfourb  42396  fourierswlem  42397  fouriersw  42398  elaa2lem  42400  etransclem15  42416  etransclem19  42420  etransclem20  42421  etransclem22  42423  etransclem23  42424  etransclem24  42425  etransclem25  42426  etransclem27  42428  etransclem28  42429  etransclem35  42436  etransclem38  42439  qndenserrnbl  42462  ioorrnopn  42472  ioorrnopnxrlem  42473  ioorrnopnxr  42474  prsal  42485  salexct  42499  issalnnd  42510  sge0sn  42543  sge0tsms  42544  sge0cl  42545  sge0f1o  42546  sge0sup  42555  sge0less  42556  sge0pr  42558  sge0prle  42565  sge0le  42571  sge0split  42573  sge0splitmpt  42575  sge0iunmptlemfi  42577  sge0iunmpt  42582  sge0isum  42591  sge0xaddlem1  42597  sge0xadd  42599  sge0gtfsumgt  42607  nnfoctbdjlem  42619  iundjiun  42624  meadjun  42626  ismeannd  42631  voliunsge0lem  42636  meaiuninc3v  42648  caragenfiiuncl  42679  omeiunltfirp  42683  carageniuncl  42687  caragenunicl  42688  isomenndlem  42694  isomennd  42695  hoicvr  42712  ovnssle  42725  ovn0  42730  ovnsubadd  42736  hsphoidmvle2  42749  hoidmvval0b  42754  hoidmv1lelem1  42755  hoidmv1lelem2  42756  hoidmv1le  42758  hoidmvlelem2  42760  hoidmvlelem3  42761  hoidmvlelem5  42763  hoidmvle  42764  ovnhoilem1  42765  ovnhoi  42767  ovnlecvr2  42774  hspdifhsp  42780  hoidifhspdmvle  42784  hoiqssbl  42789  hspmbllem1  42790  hspmbllem2  42791  hspmbl  42793  hoimbl  42795  volico2  42805  ovolval2lem  42807  ovnsubadd2lem  42809  ovolval4lem1  42813  ovolval4lem2  42814  ovolval5lem1  42816  vonhoire  42836  iunhoiioo  42840  vonioo  42846  vonicc  42849  vonsn  42855  pimrecltpos  42869  incsmflem  42900  smfpimltxr  42906  smfconst  42908  decsmflem  42924  smfpimgtxr  42938  smfrec  42946  sharhght  43004  ichnfimlem3  43471  rrx2linest  44628
  Copyright terms: Public domain W3C validator