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 828
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 169 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 196  df-an 385
This theorem is referenced by:  pm2.61ddan  829  pm2.61dda  830  nfsb4t  2377  ifeq1da  4066  ifeq2da  4067  ifeq12da  4068  ifclda  4070  ifeqda  4071  ifbothda  4073  2if2  4086  nelsnOLD  4160  somin1  5448  xpcan  5489  fvmpti  6190  fvmptss  6201  funressn  6331  ovima0  6711  oeoa  7564  oeoe  7566  omabs  7614  eceqoveq  7740  domdifsn  7928  pw2f1olem  7949  mapdom1  8010  marypha1lem  8222  supval2  8244  infdifsn  8437  carden2b  8676  fidomtri  8702  dfac12lem2  8849  cdadom1  8891  infunsdom1  8918  infunsdom  8919  itunisuc  9124  gchdomtri  9330  xrmax2  11881  xrmin1  11882  ifle  11902  xmulneg1  11971  xrsupsslem  12009  xrinfmsslem  12010  fzneuz  12290  seqf1olem1  12702  bccmpl  12958  bcval5  12967  bcpasc  12970  bccl  12971  hasheni  12998  hashfn  13025  hashdom  13029  hashdomi  13030  hashge1  13039  hashbc  13094  sumz  14300  sumss  14302  sumsplit  14341  prod1  14513  prodss  14516  fprodsplitsn  14559  fprodle  14566  bitsmod  14996  sadadd2lem2  15010  sadcaddlem  15017  gcddvds  15063  gcdcl  15066  gcdneg  15081  dvdslcm  15149  lcmcl  15152  lcmneg  15154  lcmgcd  15158  lcmfcl  15179  dvdslcmf  15182  pcgcd  15420  pcmpt  15434  pcmpt2  15435  pcprod  15437  fldivp1  15439  prmreclem4  15461  vdwlem6  15528  ramub1lem1  15568  cidpropd  16193  rescabs  16316  lubval  16807  glbval  16820  joinval  16828  meetval  16842  acsexdimd  17006  gsumpropd2lem  17096  gsumval2  17103  f1otrspeq  17690  pmtrfinv  17704  psgnunilem1  17736  gsumval3  18131  ablfac1c  18293  ablfac1eu  18295  mgpress  18323  psrbas  19199  resspsrbas  19236  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  opsrle  19296  opsrbaslem  19298  opsrbaslemOLD  19299  psrbaspropd  19426  mplbaspropd  19428  frlmsslsp  19954  mdetdiag  20224  mdetunilem7  20243  mdetunilem9  20245  maducoeval2  20265  madurid  20269  opnnei  20734  restbas  20772  hauspwdom  21114  ptcmplem5  21670  xrsmopn  22423  xrhmeo  22553  lebnum  22571  pcohtpylem  22627  pcoass  22632  pcorevlem  22634  icombl  23139  ioombl  23140  mbfconstlem  23202  mbfima  23205  i1fd  23254  mbfi1fseqlem5  23292  itg2const2  23314  itg2seq  23315  itg2uba  23316  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  iblss  23377  iblss2  23378  itgss  23384  bddmulibl  23411  coemullem  23810  aaliou2b  23900  isppw2  24641  mule1  24674  ppip1le  24687  dchrelbas3  24763  dchrpt  24792  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgslem4  24825  lgsneg  24846  lgsmod  24848  lgsdilem  24849  lgsdir  24857  lgsdi  24859  lgsne0  24860  lgsquad3  24912  dchrvmasum2if  24986  midexlem  25387  colperpex  25425  outpasch  25447  hlpasch  25448  lnopp2hpgb  25455  lmieu  25476  inaghl  25531  cgrg3col4  25534  nmcfnlbi  28295  elpreq  28744  disjdifprg  28770  disjun0  28790  f1ocnt  28946  xrge0npcan  29025  archiabl  29083  orngsqr  29135  psgnfzto1stlem  29181  1smat1  29198  esumcst  29452  esumrnmpt2  29457  hasheuni  29474  esumcvg  29475  ddemeas  29626  omssubadd  29689  eulerpartlemgc  29751  eulerpartlemb  29757  plymulx  29951  signswmnd  29960  signstfvneq0  29975  erdsze2lem1  30439  mrsubvrs  30673  trpredlem1  30971  unblimceq0lem  31667  unbdqndv2lem2  31671  knoppndvlem10  31682  wl-spae  32485  wl-cbvalnaed  32498  wl-nfeqfb  32502  unccur  32562  poimirlem15  32594  poimirlem22  32601  itg2addnclem  32631  itg2addnclem2  32632  iblmulc2nc  32645  ftc1anclem5  32659  ftc1anc  32663  dvasin  32666  areacirclem5  32674  exmid2  33071  3dim1  33771  3dim2  33772  3dim3  33773  3atlem3  33789  3atlem7  33793  lvolnle3at  33886  2lplnja  33923  paddasslem18  34141  lhpexle3lem  34315  4atex  34380  cdlemd5  34507  cdleme16  34590  cdleme20  34630  cdleme21j  34642  cdleme21  34643  cdleme32snaw  34741  cdleme32fvcl  34746  cdleme32le  34753  cdlemeg46gf  34839  cdleme48gfv  34843  cdleme50trn12  34858  cdlemg6  34929  cdlemg7N  34932  cdlemg38  35021  cdlemg46  35041  dibvalrel  35470  dihlss  35557  dihglblem5aN  35599  dihmeetbN  35610  dihmeetALTN  35634  dihatlat  35641  dihatexv  35645  dvh3dim2  35755  dvh3dim3N  35756  lclkrlem2h  35821  mapdh8d  36090  mapdh8g  36093  hdmap11lem2  36152  ttac  36621  pw2f1ocnv  36622  aomclem5  36646  isnumbasgrplem3  36694  iocmbl  36817  radcnvrat  37535  bccbc  37566  binomcxp  37578  fnchoice  38211  fiiuncl  38259  disjxp1  38263  eliin2f  38316  founiiun0  38372  axccdom  38411  axccd2  38425  fzisoeu  38455  fperiodmul  38459  upbdrech2  38463  fzdifsuc2  38466  uzfissfz  38483  supxrgere  38490  supxrgelem  38494  supxrge  38495  suplesup  38496  infrpge  38508  xrlexaddrp  38509  xralrple2  38511  infxr  38524  infleinflem1  38527  infleinflem2  38528  infleinf  38529  xralrple3  38531  fiminre2  38535  xrralrecnnge  38554  ioondisj2  38561  iccdifprioo  38589  fsumsplitsn  38637  fmul01lt1lem1  38651  fmul01lt1lem2  38652  limciccioolb  38688  lptioo2  38698  lptioo1  38699  limcicciooub  38704  lptre2pt  38707  limcresiooub  38709  limcresioolb  38710  limcleqr  38711  climfveq  38736  coskpi2  38749  cosknegpi  38752  icccncfext  38773  cncfiooicclem1  38779  cncfiooicc  38780  cncfiooiccre  38781  dvbdfbdioolem2  38819  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnxpaek  38832  dvnprodlem1  38836  dvnprodlem3  38838  volioc  38864  itgioocnicc  38869  iblcncfioo  38870  volico  38876  sublevolico  38877  ismbl3  38879  ovolsplit  38881  volioore  38883  voliooico  38885  voliccico  38892  stoweidlem14  38907  stoweidlem26  38919  stoweidlem28  38921  stoweidlem55  38948  stoweid  38956  stirlinglem5  38971  stirlinglem12  38978  dirkerper  38989  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncf  39000  fourierdlem10  39010  fourierdlem12  39012  fourierdlem24  39024  fourierdlem30  39030  fourierdlem31  39031  fourierdlem32  39032  fourierdlem33  39033  fourierdlem34  39034  fourierdlem35  39035  fourierdlem37  39037  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem43  39043  fourierdlem44  39044  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem54  39053  fourierdlem62  39061  fourierdlem64  39063  fourierdlem65  39064  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem82  39081  fourierdlem92  39091  fourierdlem93  39092  fourierdlem97  39096  fourierdlem101  39100  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem109  39108  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem15  39142  etransclem19  39146  etransclem20  39147  etransclem22  39149  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem27  39154  etransclem28  39155  etransclem35  39162  etransclem38  39165  qndenserrnbl  39191  ioorrnopn  39201  ioorrnopnxrlem  39202  ioorrnopnxr  39203  prsal  39214  salexct  39228  issalnnd  39239  sge0sn  39272  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0sup  39284  sge0less  39285  sge0pr  39287  sge0prle  39294  sge0le  39300  sge0split  39302  sge0splitmpt  39304  sge0iunmptlemfi  39306  sge0iunmpt  39311  sge0isum  39320  sge0xaddlem1  39326  sge0xadd  39328  sge0gtfsumgt  39336  nnfoctbdjlem  39348  iundjiun  39353  meadjun  39355  ismeannd  39360  voliunsge0lem  39365  caragenfiiuncl  39405  omeiunltfirp  39409  carageniuncl  39413  caragenunicl  39414  isomenndlem  39420  isomennd  39421  hoicvr  39438  ovnssle  39451  ovn0  39456  ovnsubadd  39462  hsphoidmvle2  39475  hoidmvval0b  39480  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  hspdifhsp  39506  hoidifhspdmvle  39510  hoiqssbl  39515  hspmbllem1  39516  hspmbllem2  39517  hspmbl  39519  hoimbl  39521  volico2  39531  ovolval2lem  39533  ovnsubadd2lem  39535  ovolval4lem1  39539  ovolval4lem2  39540  ovolval5lem1  39542  vonhoire  39563  iunhoiioo  39567  vonioo  39573  vonicc  39576  vonsn  39582  pimrecltpos  39596  incsmflem  39628  smfpimltxr  39634  smfconst  39636  decsmflem  39652  smfpimgtxr  39666  smfrec  39674  sharhght  39703  pthdlem1  40972
  Copyright terms: Public domain W3C validator