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 813
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 397 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61dan.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
43ex 397 . 2 (𝜑 → (¬ 𝜓𝜒))
52, 4pm2.61d 171 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 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-an 383
This theorem is referenced by:  pm2.61ddan  814  pm2.61dda  815  nfsb4t  2536  pm2.61danel  3060  ifeq1da  4255  ifeq2da  4256  ifeq12da  4257  ifclda  4259  ifeqda  4260  ifbothda  4262  2if2  4275  somin1  5670  xpcan  5711  fvmpti  6423  fvmptss  6434  funressn  6569  ovima0  6960  oeoa  7831  oeoe  7833  omabs  7881  eceqoveq  8005  domdifsn  8199  pw2f1olem  8220  mapdom1  8281  marypha1lem  8495  supval2  8517  infdifsn  8718  carden2b  8993  fidomtri  9019  dfac12lem2  9168  cdadom1  9210  infunsdom1  9237  infunsdom  9238  itunisuc  9443  gchdomtri  9653  xrmax2  12212  xrmin1  12213  ifle  12233  xmulneg1  12304  xrsupsslem  12342  xrinfmsslem  12343  fzneuz  12628  seqf1olem1  13047  bccmpl  13300  bcval5  13309  bcpasc  13312  bccl  13313  hasheni  13340  hashfn  13366  hashdom  13370  hashdomi  13371  hashge1  13380  hashbc  13439  sumz  14661  sumss  14663  fsumsplitsn  14682  sumsplit  14707  prod1  14881  prodss  14884  fprodsplitsn  14926  fprodle  14933  bitsmod  15366  sadadd2lem2  15380  sadcaddlem  15387  gcddvds  15433  gcdcl  15436  gcdneg  15451  dvdslcm  15519  lcmcl  15522  lcmneg  15524  lcmgcd  15528  lcmfcl  15549  dvdslcmf  15552  pcgcd  15789  pcmpt  15803  pcmpt2  15804  pcprod  15806  fldivp1  15808  prmreclem4  15830  vdwlem6  15897  ramub1lem1  15937  cidpropd  16577  rescabs  16700  lubval  17192  glbval  17205  joinval  17213  meetval  17227  acsexdimd  17391  gsumpropd2lem  17481  gsumval2  17488  f1otrspeq  18074  pmtrfinv  18088  psgnunilem1  18120  gsumval3  18515  ablfac1c  18678  ablfac1eu  18680  mgpress  18708  psrbas  19593  resspsrbas  19630  mplmonmul  19679  mplcoe1  19680  mplcoe5  19683  opsrle  19690  opsrbaslem  19692  opsrbaslemOLD  19693  psrbaspropd  19820  mplbaspropd  19822  frlmsslsp  20352  mdetdiag  20623  mdetunilem7  20642  mdetunilem9  20644  maducoeval2  20664  madurid  20668  opnnei  21145  restbas  21183  hauspwdom  21525  ptcmplem5  22080  xrsmopn  22835  xrhmeo  22965  lebnum  22983  pcohtpylem  23038  pcoass  23043  pcorevlem  23045  icombl  23552  ioombl  23553  mbfconstlem  23615  mbfima  23618  i1fd  23668  mbfi1fseqlem5  23706  itg2const2  23728  itg2seq  23729  itg2uba  23730  itg2splitlem  23735  itg2split  23736  itg2monolem1  23737  itg2gt0  23747  itg2cnlem1  23748  itg2cnlem2  23749  iblss  23791  iblss2  23792  itgss  23798  bddmulibl  23825  coemullem  24226  aaliou2b  24316  isppw2  25062  mule1  25095  ppip1le  25108  dchrelbas3  25184  dchrpt  25213  bposlem3  25232  bposlem5  25234  bposlem6  25235  lgslem4  25246  lgsneg  25267  lgsmod  25269  lgsdilem  25270  lgsdir  25278  lgsdi  25280  lgsne0  25281  lgsquad3  25333  dchrvmasum2if  25407  midexlem  25808  colperpex  25846  outpasch  25868  hlpasch  25869  lnopp2hpgb  25876  lmieu  25897  inaghl  25952  cgrg3col4  25955  pthdlem1  26897  nmcfnlbi  29251  elpreq  29698  disjdifprg  29726  disjun0  29746  f1ocnt  29899  xrge0npcan  30034  archiabl  30092  orngsqr  30144  psgnfzto1stlem  30190  1smat1  30210  esumcst  30465  esumrnmpt2  30470  hasheuni  30487  esumcvg  30488  ddemeas  30639  omssubadd  30702  eulerpartlemgc  30764  eulerpartlemb  30770  plymulx  30965  signswmnd  30974  signstfvneq0  30989  erdsze2lem1  31523  mrsubvrs  31757  trpredlem1  32063  unblimceq0lem  32834  unbdqndv2lem2  32838  knoppndvlem10  32849  wl-spae  33643  wl-cbvalnaed  33654  wl-nfeqfb  33658  unccur  33725  poimirlem15  33757  poimirlem22  33764  itg2addnclem  33793  itg2addnclem2  33794  iblmulc2nc  33807  ftc1anclem5  33821  ftc1anc  33825  dvasin  33828  areacirclem5  33836  exmid2  34233  3dim1  35275  3dim2  35276  3dim3  35277  3atlem3  35293  3atlem7  35297  lvolnle3at  35390  2lplnja  35427  paddasslem18  35645  lhpexle3lem  35819  4atex  35884  cdlemd5  36011  cdleme16  36094  cdleme20  36133  cdleme21j  36145  cdleme21  36146  cdleme32snaw  36244  cdleme32fvcl  36249  cdleme32le  36256  cdlemeg46gf  36342  cdleme48gfv  36346  cdleme50trn12  36361  cdlemg6  36432  cdlemg7N  36435  cdlemg38  36524  cdlemg46  36544  dibvalrel  36973  dihlss  37060  dihglblem5aN  37102  dihmeetbN  37113  dihmeetALTN  37137  dihatlat  37144  dihatexv  37148  dvh3dim2  37258  dvh3dim3N  37259  lclkrlem2h  37324  mapdh8d  37593  mapdh8g  37595  hdmap11lem2  37652  ttac  38129  pw2f1ocnv  38130  aomclem5  38154  isnumbasgrplem3  38201  iocmbl  38324  radcnvrat  39039  bccbc  39070  binomcxp  39082  fnchoice  39710  fiiuncl  39755  disjxp1  39759  eliin2f  39808  founiiun0  39897  axccdom  39934  axccd2  39948  fzisoeu  40031  fperiodmul  40035  upbdrech2  40039  fzdifsuc2  40041  uzfissfz  40058  supxrgere  40065  supxrgelem  40069  supxrge  40070  suplesup  40071  infrpge  40083  xrlexaddrp  40084  xralrple2  40086  infxr  40099  infleinflem1  40102  infleinflem2  40103  infleinf  40104  xralrple3  40106  fiminre2  40110  xrralrecnnge  40129  uzublem  40173  supxrmnf2  40176  infxrpnf  40190  infxrpnf2  40209  supminfxr  40210  supminfxr2  40215  ioondisj2  40235  iccdifprioo  40261  fmul01lt1lem1  40334  fmul01lt1lem2  40335  limciccioolb  40371  lptioo2  40381  lptioo1  40382  limcicciooub  40387  lptre2pt  40390  limcresiooub  40392  limcresioolb  40393  limcleqr  40394  climfveq  40419  climfveqf  40430  limsupubuzlem  40462  limsupubuz  40463  limsupmnfuzlem  40476  limsupre3uzlem  40485  climxrre  40500  limsup10exlem  40522  cnrefiisplem  40573  climxlim2lem  40589  dfxlim2v  40591  coskpi2  40595  cosknegpi  40598  icccncfext  40618  cncfiooicclem1  40624  cncfiooicc  40625  cncfiooiccre  40626  dvbdfbdioolem2  40662  ioodvbdlimc1lem1  40664  ioodvbdlimc1lem2  40665  ioodvbdlimc2lem  40667  dvnxpaek  40675  dvnprodlem1  40679  dvnprodlem3  40681  volioc  40705  itgioocnicc  40710  iblcncfioo  40711  volico  40717  sublevolico  40718  ismbl3  40720  ovolsplit  40722  volioore  40724  voliooico  40726  voliccico  40733  stoweidlem14  40748  stoweidlem26  40760  stoweidlem28  40762  stoweidlem55  40789  stoweid  40797  stirlinglem5  40812  stirlinglem12  40819  dirkerper  40830  dirkertrigeqlem3  40834  dirkertrigeq  40835  dirkercncflem1  40837  dirkercncflem2  40838  dirkercncf  40841  fourierdlem10  40851  fourierdlem12  40853  fourierdlem24  40865  fourierdlem30  40871  fourierdlem31  40872  fourierdlem32  40873  fourierdlem33  40874  fourierdlem34  40875  fourierdlem35  40876  fourierdlem37  40878  fourierdlem40  40881  fourierdlem41  40882  fourierdlem42  40883  fourierdlem43  40884  fourierdlem44  40885  fourierdlem46  40886  fourierdlem48  40888  fourierdlem49  40889  fourierdlem51  40891  fourierdlem54  40894  fourierdlem62  40902  fourierdlem64  40904  fourierdlem65  40905  fourierdlem70  40910  fourierdlem71  40911  fourierdlem73  40913  fourierdlem74  40914  fourierdlem75  40915  fourierdlem78  40918  fourierdlem79  40919  fourierdlem80  40920  fourierdlem81  40921  fourierdlem82  40922  fourierdlem92  40932  fourierdlem93  40933  fourierdlem97  40937  fourierdlem101  40941  fourierdlem102  40942  fourierdlem103  40943  fourierdlem104  40944  fourierdlem109  40949  fourierdlem114  40954  sqwvfoura  40962  sqwvfourb  40963  fourierswlem  40964  fouriersw  40965  elaa2lem  40967  etransclem15  40983  etransclem19  40987  etransclem20  40988  etransclem22  40990  etransclem23  40991  etransclem24  40992  etransclem25  40993  etransclem27  40995  etransclem28  40996  etransclem35  41003  etransclem38  41006  qndenserrnbl  41032  ioorrnopn  41042  ioorrnopnxrlem  41043  ioorrnopnxr  41044  prsal  41055  salexct  41069  issalnnd  41080  sge0sn  41113  sge0tsms  41114  sge0cl  41115  sge0f1o  41116  sge0sup  41125  sge0less  41126  sge0pr  41128  sge0prle  41135  sge0le  41141  sge0split  41143  sge0splitmpt  41145  sge0iunmptlemfi  41147  sge0iunmpt  41152  sge0isum  41161  sge0xaddlem1  41167  sge0xadd  41169  sge0gtfsumgt  41177  nnfoctbdjlem  41189  iundjiun  41194  meadjun  41196  ismeannd  41201  voliunsge0lem  41206  meaiuninc3v  41218  caragenfiiuncl  41249  omeiunltfirp  41253  carageniuncl  41257  caragenunicl  41258  isomenndlem  41264  isomennd  41265  hoicvr  41282  ovnssle  41295  ovn0  41300  ovnsubadd  41306  hsphoidmvle2  41319  hoidmvval0b  41324  hoidmv1lelem1  41325  hoidmv1lelem2  41326  hoidmv1le  41328  hoidmvlelem2  41330  hoidmvlelem3  41331  hoidmvlelem5  41333  hoidmvle  41334  ovnhoilem1  41335  ovnhoi  41337  ovnlecvr2  41344  hspdifhsp  41350  hoidifhspdmvle  41354  hoiqssbl  41359  hspmbllem1  41360  hspmbllem2  41361  hspmbl  41363  hoimbl  41365  volico2  41375  ovolval2lem  41377  ovnsubadd2lem  41379  ovolval4lem1  41383  ovolval4lem2  41384  ovolval5lem1  41386  vonhoire  41406  iunhoiioo  41410  vonioo  41416  vonicc  41419  vonsn  41425  pimrecltpos  41439  incsmflem  41470  smfpimltxr  41476  smfconst  41478  decsmflem  41494  smfpimgtxr  41508  smfrec  41516  sharhght  41574
  Copyright terms: Public domain W3C validator