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 849
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 449 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61dan.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
43ex 449 . 2 (𝜑 → (¬ 𝜓𝜒))
52, 4pm2.61d 170 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 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-an 385
This theorem is referenced by:  pm2.61ddan  850  pm2.61dda  851  nfsb4t  2417  pm2.61danel  2940  ifeq1da  4149  ifeq2da  4150  ifeq12da  4151  ifclda  4153  ifeqda  4154  ifbothda  4156  2if2  4169  somin1  5564  xpcan  5605  fvmpti  6320  fvmptss  6331  funressn  6466  ovima0  6855  oeoa  7722  oeoe  7724  omabs  7772  eceqoveq  7895  domdifsn  8084  pw2f1olem  8105  mapdom1  8166  marypha1lem  8380  supval2  8402  infdifsn  8592  carden2b  8831  fidomtri  8857  dfac12lem2  9004  cdadom1  9046  infunsdom1  9073  infunsdom  9074  itunisuc  9279  gchdomtri  9489  xrmax2  12045  xrmin1  12046  ifle  12066  xmulneg1  12137  xrsupsslem  12175  xrinfmsslem  12176  fzneuz  12459  seqf1olem1  12880  bccmpl  13136  bcval5  13145  bcpasc  13148  bccl  13149  hasheni  13176  hashfn  13202  hashdom  13206  hashdomi  13207  hashge1  13216  hashbc  13275  sumz  14497  sumss  14499  fsumsplitsn  14518  sumsplit  14543  prod1  14718  prodss  14721  fprodsplitsn  14764  fprodle  14771  bitsmod  15205  sadadd2lem2  15219  sadcaddlem  15226  gcddvds  15272  gcdcl  15275  gcdneg  15290  dvdslcm  15358  lcmcl  15361  lcmneg  15363  lcmgcd  15367  lcmfcl  15388  dvdslcmf  15391  pcgcd  15629  pcmpt  15643  pcmpt2  15644  pcprod  15646  fldivp1  15648  prmreclem4  15670  vdwlem6  15737  ramub1lem1  15777  cidpropd  16417  rescabs  16540  lubval  17031  glbval  17044  joinval  17052  meetval  17066  acsexdimd  17230  gsumpropd2lem  17320  gsumval2  17327  f1otrspeq  17913  pmtrfinv  17927  psgnunilem1  17959  gsumval3  18354  ablfac1c  18516  ablfac1eu  18518  mgpress  18546  psrbas  19426  resspsrbas  19463  mplmonmul  19512  mplcoe1  19513  mplcoe5  19516  opsrle  19523  opsrbaslem  19525  opsrbaslemOLD  19526  psrbaspropd  19653  mplbaspropd  19655  frlmsslsp  20183  mdetdiag  20453  mdetunilem7  20472  mdetunilem9  20474  maducoeval2  20494  madurid  20498  opnnei  20972  restbas  21010  hauspwdom  21352  ptcmplem5  21907  xrsmopn  22662  xrhmeo  22792  lebnum  22810  pcohtpylem  22865  pcoass  22870  pcorevlem  22872  icombl  23378  ioombl  23379  mbfconstlem  23441  mbfima  23444  i1fd  23493  mbfi1fseqlem5  23531  itg2const2  23553  itg2seq  23554  itg2uba  23555  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  iblss  23616  iblss2  23617  itgss  23623  bddmulibl  23650  coemullem  24051  aaliou2b  24141  isppw2  24886  mule1  24919  ppip1le  24932  dchrelbas3  25008  dchrpt  25037  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgslem4  25070  lgsneg  25091  lgsmod  25093  lgsdilem  25094  lgsdir  25102  lgsdi  25104  lgsne0  25105  lgsquad3  25157  dchrvmasum2if  25231  midexlem  25632  colperpex  25670  outpasch  25692  hlpasch  25693  lnopp2hpgb  25700  lmieu  25721  inaghl  25776  cgrg3col4  25779  pthdlem1  26718  nmcfnlbi  29039  elpreq  29486  disjdifprg  29514  disjun0  29534  f1ocnt  29687  xrge0npcan  29822  archiabl  29880  orngsqr  29932  psgnfzto1stlem  29978  1smat1  29998  esumcst  30253  esumrnmpt2  30258  hasheuni  30275  esumcvg  30276  ddemeas  30427  omssubadd  30490  eulerpartlemgc  30552  eulerpartlemb  30558  plymulx  30753  signswmnd  30762  signstfvneq0  30777  erdsze2lem1  31311  mrsubvrs  31545  trpredlem1  31851  unblimceq0lem  32622  unbdqndv2lem2  32626  knoppndvlem10  32637  wl-spae  33436  wl-cbvalnaed  33449  wl-nfeqfb  33453  unccur  33522  poimirlem15  33554  poimirlem22  33561  itg2addnclem  33591  itg2addnclem2  33592  iblmulc2nc  33605  ftc1anclem5  33619  ftc1anc  33623  dvasin  33626  areacirclem5  33634  exmid2  34031  3dim1  35071  3dim2  35072  3dim3  35073  3atlem3  35089  3atlem7  35093  lvolnle3at  35186  2lplnja  35223  paddasslem18  35441  lhpexle3lem  35615  4atex  35680  cdlemd5  35807  cdleme16  35890  cdleme20  35929  cdleme21j  35941  cdleme21  35942  cdleme32snaw  36040  cdleme32fvcl  36045  cdleme32le  36052  cdlemeg46gf  36138  cdleme48gfv  36142  cdleme50trn12  36157  cdlemg6  36228  cdlemg7N  36231  cdlemg38  36320  cdlemg46  36340  dibvalrel  36769  dihlss  36856  dihglblem5aN  36898  dihmeetbN  36909  dihmeetALTN  36933  dihatlat  36940  dihatexv  36944  dvh3dim2  37054  dvh3dim3N  37055  lclkrlem2h  37120  mapdh8d  37389  mapdh8g  37392  hdmap11lem2  37451  ttac  37920  pw2f1ocnv  37921  aomclem5  37945  isnumbasgrplem3  37992  iocmbl  38115  radcnvrat  38830  bccbc  38861  binomcxp  38873  fnchoice  39502  fiiuncl  39548  disjxp1  39552  eliin2f  39601  founiiun0  39691  axccdom  39730  axccd2  39744  fzisoeu  39828  fperiodmul  39832  upbdrech2  39836  fzdifsuc2  39838  uzfissfz  39855  supxrgere  39862  supxrgelem  39866  supxrge  39867  suplesup  39868  infrpge  39880  xrlexaddrp  39881  xralrple2  39883  infxr  39896  infleinflem1  39899  infleinflem2  39900  infleinf  39901  xralrple3  39903  fiminre2  39907  xrralrecnnge  39926  uzublem  39970  supxrmnf2  39973  infxrpnf  39987  infxrpnf2  40006  supminfxr  40007  supminfxr2  40012  ioondisj2  40032  iccdifprioo  40060  fmul01lt1lem1  40134  fmul01lt1lem2  40135  limciccioolb  40171  lptioo2  40181  lptioo1  40182  limcicciooub  40187  lptre2pt  40190  limcresiooub  40192  limcresioolb  40193  limcleqr  40194  climfveq  40219  climfveqf  40230  limsupubuzlem  40262  limsupubuz  40263  limsupmnfuzlem  40276  limsupre3uzlem  40285  climxrre  40300  limsup10exlem  40322  cnrefiisplem  40373  climxlim2lem  40389  dfxlim2v  40391  coskpi2  40395  cosknegpi  40398  icccncfext  40418  cncfiooicclem1  40424  cncfiooicc  40425  cncfiooiccre  40426  dvbdfbdioolem2  40462  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnxpaek  40475  dvnprodlem1  40479  dvnprodlem3  40481  volioc  40506  itgioocnicc  40511  iblcncfioo  40512  volico  40518  sublevolico  40519  ismbl3  40521  ovolsplit  40523  volioore  40525  voliooico  40527  voliccico  40534  stoweidlem14  40549  stoweidlem26  40561  stoweidlem28  40563  stoweidlem55  40590  stoweid  40598  stirlinglem5  40613  stirlinglem12  40620  dirkerper  40631  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncf  40642  fourierdlem10  40652  fourierdlem12  40654  fourierdlem24  40666  fourierdlem30  40672  fourierdlem31  40673  fourierdlem32  40674  fourierdlem33  40675  fourierdlem34  40676  fourierdlem35  40677  fourierdlem37  40679  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem43  40685  fourierdlem44  40686  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem54  40695  fourierdlem62  40703  fourierdlem64  40705  fourierdlem65  40706  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem79  40720  fourierdlem80  40721  fourierdlem81  40722  fourierdlem82  40723  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem101  40742  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem109  40750  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  elaa2lem  40768  etransclem15  40784  etransclem19  40788  etransclem20  40789  etransclem22  40791  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem27  40796  etransclem28  40797  etransclem35  40804  etransclem38  40807  qndenserrnbl  40833  ioorrnopn  40843  ioorrnopnxrlem  40844  ioorrnopnxr  40845  prsal  40856  salexct  40870  issalnnd  40881  sge0sn  40914  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0sup  40926  sge0less  40927  sge0pr  40929  sge0prle  40936  sge0le  40942  sge0split  40944  sge0splitmpt  40946  sge0iunmptlemfi  40948  sge0iunmpt  40953  sge0isum  40962  sge0xaddlem1  40968  sge0xadd  40970  sge0gtfsumgt  40978  nnfoctbdjlem  40990  iundjiun  40995  meadjun  40997  ismeannd  41002  voliunsge0lem  41007  meaiuninc3v  41019  caragenfiiuncl  41050  omeiunltfirp  41054  carageniuncl  41058  caragenunicl  41059  isomenndlem  41065  isomennd  41066  hoicvr  41083  ovnssle  41096  ovn0  41101  ovnsubadd  41107  hsphoidmvle2  41120  hoidmvval0b  41125  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1le  41129  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  hspdifhsp  41151  hoidifhspdmvle  41155  hoiqssbl  41160  hspmbllem1  41161  hspmbllem2  41162  hspmbl  41164  hoimbl  41166  volico2  41176  ovolval2lem  41178  ovnsubadd2lem  41180  ovolval4lem1  41184  ovolval4lem2  41185  ovolval5lem1  41187  vonhoire  41207  iunhoiioo  41211  vonioo  41217  vonicc  41220  vonsn  41226  pimrecltpos  41240  incsmflem  41271  smfpimltxr  41277  smfconst  41279  decsmflem  41295  smfpimgtxr  41309  smfrec  41317  sharhght  41375
  Copyright terms: Public domain W3C validator