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 838
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 399 . 2 (𝜑 → (𝜓𝜒))
3 pm2.61dan.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
43ex 399 . 2 (𝜑 → (¬ 𝜓𝜒))
52, 4pm2.61d 171 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 198  df-an 385
This theorem is referenced by:  pm2.61ddan  839  pm2.61dda  840  nfsb4t  2548  pm2.61danel  3095  ifeq1da  4309  ifeq2da  4310  ifeq12da  4311  ifclda  4313  ifeqda  4314  ifbothda  4316  2if2  4332  somin1  5740  xpcan  5781  fvmpti  6498  fvmptss  6509  funressn  6646  ovima0  7039  oeoa  7910  oeoe  7912  omabs  7960  eceqoveq  8084  domdifsn  8278  pw2f1olem  8299  mapdom1  8360  marypha1lem  8574  supval2  8596  infdifsn  8797  carden2b  9072  fidomtri  9098  dfac12lem2  9247  cdadom1  9289  infunsdom1  9316  infunsdom  9317  itunisuc  9522  gchdomtri  9732  xrmax2  12221  xrmin1  12222  ifle  12242  xmulneg1  12313  xrsupsslem  12351  xrinfmsslem  12352  fzneuz  12640  seqf1olem1  13059  bccmpl  13312  bcval5  13321  bcpasc  13324  bccl  13325  hasheni  13352  hashfn  13378  hashdom  13382  hashdomi  13383  hashge1  13392  hashbc  13450  sumz  14672  sumss  14674  fsumsplitsn  14693  sumsplit  14718  prod1  14891  prodss  14894  fprodsplitsn  14936  fprodle  14943  bitsmod  15373  sadadd2lem2  15387  sadcaddlem  15394  gcddvds  15440  gcdcl  15443  gcdneg  15458  dvdslcm  15526  lcmcl  15529  lcmneg  15531  lcmgcd  15535  lcmfcl  15556  dvdslcmf  15559  pcgcd  15795  pcmpt  15809  pcmpt2  15810  pcprod  15812  fldivp1  15814  prmreclem4  15836  vdwlem6  15903  ramub1lem1  15943  cidpropd  16570  rescabs  16693  lubval  17185  glbval  17198  joinval  17206  meetval  17220  acsexdimd  17384  gsumpropd2lem  17474  gsumval2  17481  f1otrspeq  18064  pmtrfinv  18078  psgnunilem1  18110  gsumval3  18505  ablfac1c  18668  ablfac1eu  18670  mgpress  18698  psrbas  19583  resspsrbas  19620  mplmonmul  19669  mplcoe1  19670  mplcoe5  19673  opsrle  19680  opsrbaslem  19682  psrbaspropd  19809  mplbaspropd  19811  frlmsslsp  20342  mdetdiag  20613  mdetunilem7  20632  mdetunilem9  20634  maducoeval2  20654  madurid  20658  opnnei  21135  restbas  21173  hauspwdom  21515  ptcmplem5  22070  xrsmopn  22825  xrhmeo  22955  lebnum  22973  pcohtpylem  23028  pcoass  23033  pcorevlem  23035  icombl  23544  ioombl  23545  mbfconstlem  23607  mbfima  23610  i1fd  23661  mbfi1fseqlem5  23699  itg2const2  23721  itg2seq  23722  itg2uba  23723  itg2splitlem  23728  itg2split  23729  itg2monolem1  23730  itg2gt0  23740  itg2cnlem1  23741  itg2cnlem2  23742  iblss  23784  iblss2  23785  itgss  23791  bddmulibl  23818  coemullem  24219  aaliou2b  24309  isppw2  25054  mule1  25087  ppip1le  25100  dchrelbas3  25176  dchrpt  25205  bposlem3  25224  bposlem5  25226  bposlem6  25227  lgslem4  25238  lgsneg  25259  lgsmod  25261  lgsdilem  25262  lgsdir  25270  lgsdi  25272  lgsne0  25273  lgsquad3  25325  dchrvmasum2if  25399  midexlem  25800  colperpex  25838  outpasch  25860  hlpasch  25861  lnopp2hpgb  25868  lmieu  25889  inaghl  25944  cgrg3col4  25947  pthdlem1  26889  nmcfnlbi  29238  elpreq  29684  disjdifprg  29712  disjun0  29732  f1ocnt  29885  xrge0npcan  30018  archiabl  30076  orngsqr  30128  psgnfzto1stlem  30174  1smat1  30194  esumcst  30449  esumrnmpt2  30454  hasheuni  30471  esumcvg  30472  ddemeas  30623  omssubadd  30686  eulerpartlemgc  30748  eulerpartlemb  30754  plymulx  30949  signswmnd  30958  signstfvneq0  30973  erdsze2lem1  31506  mrsubvrs  31740  trpredlem1  32045  unblimceq0lem  32812  unbdqndv2lem2  32816  knoppndvlem10  32827  wl-spae  33620  wl-cbvalnaed  33631  wl-nfeqfb  33635  unccur  33703  poimirlem15  33735  poimirlem22  33742  itg2addnclem  33771  itg2addnclem2  33772  iblmulc2nc  33785  ftc1anclem5  33799  ftc1anc  33803  dvasin  33806  areacirclem5  33814  exmid2  34210  3dim1  35245  3dim2  35246  3dim3  35247  3atlem3  35263  3atlem7  35267  lvolnle3at  35360  2lplnja  35397  paddasslem18  35615  lhpexle3lem  35789  4atex  35854  cdlemd5  35980  cdleme16  36063  cdleme20  36102  cdleme21j  36114  cdleme21  36115  cdleme32snaw  36213  cdleme32fvcl  36218  cdleme32le  36225  cdlemeg46gf  36311  cdleme48gfv  36315  cdleme50trn12  36330  cdlemg6  36401  cdlemg7N  36404  cdlemg38  36493  cdlemg46  36513  dibvalrel  36941  dihlss  37028  dihglblem5aN  37070  dihmeetbN  37081  dihmeetALTN  37105  dihatlat  37112  dihatexv  37116  dvh3dim2  37226  dvh3dim3N  37227  lclkrlem2h  37292  mapdh8d  37561  mapdh8g  37563  hdmap11lem2  37620  ttac  38101  pw2f1ocnv  38102  aomclem5  38126  isnumbasgrplem3  38173  iocmbl  38295  radcnvrat  39010  bccbc  39041  binomcxp  39053  fnchoice  39679  fiiuncl  39724  disjxp1  39728  eliin2f  39776  founiiun0  39863  axccdom  39900  axccd2  39911  fzisoeu  39992  fperiodmul  39996  upbdrech2  40000  fzdifsuc2  40002  uzfissfz  40019  supxrgere  40026  supxrgelem  40030  supxrge  40031  suplesup  40032  infrpge  40044  xrlexaddrp  40045  xralrple2  40047  infxr  40060  infleinflem1  40063  infleinflem2  40064  infleinf  40065  xralrple3  40067  fiminre2  40071  xrralrecnnge  40089  uzublem  40133  supxrmnf2  40136  infxrpnf  40150  infxrpnf2  40169  supminfxr  40170  supminfxr2  40175  ioondisj2  40195  iccdifprioo  40220  fmul01lt1lem1  40293  fmul01lt1lem2  40294  limciccioolb  40330  lptioo2  40340  lptioo1  40341  limcicciooub  40346  lptre2pt  40349  limcresiooub  40351  limcresioolb  40352  limcleqr  40353  climfveq  40378  climfveqf  40389  limsupubuzlem  40421  limsupubuz  40422  limsupmnfuzlem  40435  limsupre3uzlem  40444  climxrre  40459  limsup10exlem  40481  cnrefiisplem  40532  climxlim2lem  40548  dfxlim2v  40550  coskpi2  40554  cosknegpi  40557  icccncfext  40577  cncfiooicclem1  40583  cncfiooicc  40584  cncfiooiccre  40585  dvbdfbdioolem2  40621  ioodvbdlimc1lem1  40623  ioodvbdlimc1lem2  40624  ioodvbdlimc2lem  40626  dvnxpaek  40634  dvnprodlem1  40638  dvnprodlem3  40640  volioc  40664  itgioocnicc  40669  iblcncfioo  40670  volico  40676  sublevolico  40677  ismbl3  40679  ovolsplit  40681  volioore  40683  voliooico  40685  voliccico  40692  stoweidlem14  40707  stoweidlem26  40719  stoweidlem28  40721  stoweidlem55  40748  stoweid  40756  stirlinglem5  40771  stirlinglem12  40778  dirkerper  40789  dirkertrigeqlem3  40793  dirkertrigeq  40794  dirkercncflem1  40796  dirkercncflem2  40797  dirkercncf  40800  fourierdlem10  40810  fourierdlem12  40812  fourierdlem24  40824  fourierdlem30  40830  fourierdlem31  40831  fourierdlem32  40832  fourierdlem33  40833  fourierdlem34  40834  fourierdlem35  40835  fourierdlem37  40837  fourierdlem40  40840  fourierdlem41  40841  fourierdlem42  40842  fourierdlem43  40843  fourierdlem44  40844  fourierdlem46  40845  fourierdlem48  40847  fourierdlem49  40848  fourierdlem51  40850  fourierdlem54  40853  fourierdlem62  40861  fourierdlem64  40863  fourierdlem65  40864  fourierdlem70  40869  fourierdlem71  40870  fourierdlem73  40872  fourierdlem74  40873  fourierdlem75  40874  fourierdlem78  40877  fourierdlem79  40878  fourierdlem80  40879  fourierdlem81  40880  fourierdlem82  40881  fourierdlem92  40891  fourierdlem93  40892  fourierdlem97  40896  fourierdlem101  40900  fourierdlem102  40901  fourierdlem103  40902  fourierdlem104  40903  fourierdlem109  40908  fourierdlem114  40913  sqwvfoura  40921  sqwvfourb  40922  fourierswlem  40923  fouriersw  40924  elaa2lem  40926  etransclem15  40942  etransclem19  40946  etransclem20  40947  etransclem22  40949  etransclem23  40950  etransclem24  40951  etransclem25  40952  etransclem27  40954  etransclem28  40955  etransclem35  40962  etransclem38  40965  qndenserrnbl  40991  ioorrnopn  41001  ioorrnopnxrlem  41002  ioorrnopnxr  41003  prsal  41014  salexct  41028  issalnnd  41039  sge0sn  41072  sge0tsms  41073  sge0cl  41074  sge0f1o  41075  sge0sup  41084  sge0less  41085  sge0pr  41087  sge0prle  41094  sge0le  41100  sge0split  41102  sge0splitmpt  41104  sge0iunmptlemfi  41106  sge0iunmpt  41111  sge0isum  41120  sge0xaddlem1  41126  sge0xadd  41128  sge0gtfsumgt  41136  nnfoctbdjlem  41148  iundjiun  41153  meadjun  41155  ismeannd  41160  voliunsge0lem  41165  meaiuninc3v  41177  caragenfiiuncl  41208  omeiunltfirp  41212  carageniuncl  41216  caragenunicl  41217  isomenndlem  41223  isomennd  41224  hoicvr  41241  ovnssle  41254  ovn0  41259  ovnsubadd  41265  hsphoidmvle2  41278  hoidmvval0b  41283  hoidmv1lelem1  41284  hoidmv1lelem2  41285  hoidmv1le  41287  hoidmvlelem2  41289  hoidmvlelem3  41290  hoidmvlelem5  41292  hoidmvle  41293  ovnhoilem1  41294  ovnhoi  41296  ovnlecvr2  41303  hspdifhsp  41309  hoidifhspdmvle  41313  hoiqssbl  41318  hspmbllem1  41319  hspmbllem2  41320  hspmbl  41322  hoimbl  41324  volico2  41334  ovolval2lem  41336  ovnsubadd2lem  41338  ovolval4lem1  41342  ovolval4lem2  41343  ovolval5lem1  41345  vonhoire  41365  iunhoiioo  41369  vonioo  41375  vonicc  41378  vonsn  41384  pimrecltpos  41398  incsmflem  41429  smfpimltxr  41435  smfconst  41437  decsmflem  41453  smfpimgtxr  41467  smfrec  41475  sharhght  41533
  Copyright terms: Public domain W3C validator