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

Step	Hyp	Ref	Expression
1		pm2.61dan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61dan.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
4	3	ex 412	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
5	2, 4	pm2.61d 179	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm2.61ddan  814  pm2.61dda  815  nfsb4t  2504  sbal2  2534  pm2.61danel  3051  ifeq1da  4513  ifeq2da  4514  ifeq12da  4515  ifclda  4517  ifeqda  4518  ifbothda  4520  2if2  4537  somin1  6098  xpcan  6142  fvmpti  6948  fvmptss  6962  funressn  7114  ovima0  7547  ordsuci  7763  suppssov1  8149  suppssov2  8150  oeoa  8535  oeoe  8537  omabs  8589  eceqoveq  8771  domdifsn  9000  pw2f1olem  9021  mapdom1  9082  imafiOLD  9228  marypha1lem  9348  supval2  9370  infdifsn  9578  ttrcltr  9637  ttrclselem1  9646  carden2b  9891  fidomtri  9917  dfac12lem2  10067  infunsdom1  10134  infunsdom  10135  itunisuc  10341  gchdomtri  10552  fiminre2  12102  xrmax2  13103  xrmin1  13104  ifle  13124  xnn0lem1lt  13171  xmulneg1  13196  xrsupsslem  13234  xrinfmsslem  13235  fzneuz  13536  seqf1olem1  13976  bccmpl  14244  bcval5  14253  bcpasc  14256  bccl  14257  hasheni  14283  hashfn  14310  hashdom  14314  hashdomi  14315  hashge1  14324  hashbc  14388  pfxval0  14612  sumz  15657  sumss  15659  fsumsplitsn  15679  sumsplit  15703  prod1  15879  prodss  15882  fprodsplitsn  15924  fprodle  15931  bitsmod  16375  sadadd2lem2  16389  sadcaddlem  16396  gcddvds  16442  gcdcl  16445  gcdneg  16461  dvdslcm  16537  lcmcl  16540  lcmneg  16542  lcmgcd  16546  lcmfcl  16567  dvdslcmf  16570  pcgcd  16818  pcmpt  16832  pcmpt2  16833  pcprod  16835  fldivp1  16837  prmreclem4  16859  vdwlem6  16926  ramub1lem1  16966  cidpropd  17645  rescabs  17769  lubval  18289  glbval  18302  joinval  18310  meetval  18324  acsexdimd  18494  gsumpropd2lem  18616  gsumval2  18623  mulgfval  19011  f1otrspeq  19388  pmtrfinv  19402  psgnunilem1  19434  gsumval3  19848  ablfac1c  20014  ablfac1eu  20016  mgpress  20097  orngsqr  20811  frlmsslsp  21763  psrbas  21901  resspsrbas  21941  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  opsrle  22014  opsrbaslem  22016  psrbaspropd  22187  mplbaspropd  22189  mdetdiag  22555  mdetunilem7  22574  mdetunilem9  22576  maducoeval2  22596  madurid  22600  opnnei  23076  restbas  23114  hauspwdom  23457  ptcmplem5  24012  xrsmopn  24769  xrhmeo  24912  lebnum  24931  pcoass  24992  pcorevlem  24994  icombl  25533  ioombl  25534  mbfconstlem  25596  mbfima  25599  i1fd  25650  mbfi1fseqlem5  25688  itg2const2  25710  itg2seq  25711  itg2uba  25712  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  iblss  25774  iblss2  25775  itgss  25781  bddmulibl  25808  coemullem  26223  aaliou2b  26317  isppw2  27093  mule1  27126  ppip1le  27139  dchrelbas3  27217  dchrpt  27246  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgslem4  27279  lgsneg  27300  lgsmod  27302  lgsdilem  27303  lgsdir  27311  lgsdi  27313  lgsne0  27314  lgsquad3  27366  dchrvmasum2if  27476  maxs2  27750  mins1  27751  z12bday  28493  midexlem  28776  colperpex  28817  outpasch  28839  hlpasch  28840  lnopp2hpgb  28847  lmieu  28868  inaghl  28929  cgrg3col4  28937  pthdlem1  29851  nmcfnlbi  32139  elpreq  32614  prssad  32615  prssbd  32616  disjdifprg  32661  disjun0  32681  argcj  32838  f1ocnt  32890  xrge0npcan  33112  psgnfzto1stlem  33193  cyc3genpmlem  33244  cyc3conja  33250  archiabl  33291  erlval  33351  1arithufdlem3  33638  1arithufd  33640  psrmonmul  33726  esplyfval3  33748  resssra  33763  lbslelsp  33774  constrrecl  33946  constrinvcl  33950  constrsqrtcl  33956  1smat1  33981  esumcst  34240  esumrnmpt2  34245  hasheuni  34262  esumcvg  34263  ddemeas  34413  omssubadd  34477  eulerpartlemgc  34539  eulerpartlemb  34545  plymulx  34725  signswmnd  34734  fineqvnttrclselem1  35296  pthhashvtx  35341  erdsze2lem1  35416  mrsubvrs  35735  unblimceq0lem  36725  unbdqndv2lem2  36729  knoppndvlem10  36740  wl-spae  37770  wl-cbvalnaed  37781  wl-nfeqfb  37785  unccur  37848  poimirlem15  37880  poimirlem22  37887  itg2addnclem  37916  itg2addnclem2  37917  iblmulc2nc  37930  ftc1anclem5  37942  ftc1anc  37946  dvasin  37949  areacirclem5  37957  exmid2  38344  3dim1  39837  3dim2  39838  3dim3  39839  3atlem3  39855  3atlem7  39859  lvolnle3at  39952  2lplnja  39989  paddasslem18  40207  lhpexle3lem  40381  4atex  40446  cdlemd5  40572  cdleme16  40655  cdleme20  40694  cdleme21j  40706  cdleme21  40707  cdleme32snaw  40805  cdleme32fvcl  40810  cdleme32le  40817  cdlemeg46gf  40903  cdleme48gfv  40907  cdleme50trn12  40922  cdlemg6  40993  cdlemg7N  40996  cdlemg38  41085  cdlemg46  41105  dibvalrel  41533  dihlss  41620  dihglblem5aN  41662  dihmeetbN  41673  dihmeetALTN  41697  dihatlat  41704  dihatexv  41708  dvh3dim2  41818  dvh3dim3N  41819  lclkrlem2h  41884  mapdh8d  42153  mapdh8g  42155  hdmap11lem2  42212  lcmineqlem23  42415  aks4d1p3  42442  aks4d1p5  42444  aks4d1p7d1  42446  posbezout  42464  aks6d1c2p2  42483  aks6d1c4  42488  aks6d1c5lem1  42500  aks6d1c6lem3  42536  aks6d1c6lem4  42537  bcled  42542  bcle2d  42543  aks6d1c7  42548  grpods  42558  unitscyglem2  42560  unitscyglem4  42562  aks5lem8  42565  dffltz  42986  ttac  43387  pw2f1ocnv  43388  aomclem5  43409  isnumbasgrplem3  43456  iocmbl  43564  oe0suclim  43628  tfsconcatfv  43692  safesnsupfidom1o  43767  safesnsupfilb  43768  r1rankcld  44581  grur1cld  44582  grucollcld  44610  mnuprd  44626  radcnvrat  44664  bccbc  44695  binomcxp  44707  fnchoice  45383  fiiuncl  45419  eliin2f  45457  founiiun0  45543  axccdom  45574  axccd2  45582  fzisoeu  45656  fperiodmul  45660  upbdrech2  45664  fzdifsuc2  45666  uzfissfz  45679  supxrgere  45686  supxrgelem  45690  supxrge  45691  suplesup  45692  infrpge  45704  xrlexaddrp  45705  xralrple2  45707  infxr  45719  infleinflem1  45722  infleinflem2  45723  infleinf  45724  xralrple3  45726  xrralrecnnge  45742  uzublem  45782  supxrmnf2  45785  infxrpnf  45798  infxrpnf2  45815  supminfxr  45816  supminfxr2  45821  pimxrneun  45840  rexanuz2nf  45844  ioondisj2  45847  iccdifprioo  45870  fmul01lt1lem1  45938  fmul01lt1lem2  45939  limciccioolb  45975  lptioo2  45985  lptioo1  45986  limcicciooub  45989  lptre2pt  45992  limcresiooub  45994  limcresioolb  45995  limcleqr  45996  climfveq  46021  climfveqf  46032  limsupubuzlem  46064  limsupubuz  46065  limsupmnfuzlem  46078  limsupre3uzlem  46087  climxrre  46102  limsup10exlem  46124  cnrefiisplem  46181  climxlim2lem  46197  dfxlim2v  46199  xlimliminflimsup  46214  coskpi2  46218  cosknegpi  46221  icccncfext  46239  cncfiooicclem1  46245  cncfiooicc  46246  cncfiooiccre  46247  dvbdfbdioolem2  46281  ioodvbdlimc1lem1  46283  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvnxpaek  46294  dvnprodlem1  46298  dvnprodlem3  46300  volioc  46324  itgioocnicc  46329  iblcncfioo  46330  volico  46335  sublevolico  46336  ismbl3  46338  ovolsplit  46340  volioore  46342  voliooico  46344  voliccico  46351  stoweidlem14  46366  stoweidlem26  46378  stoweidlem28  46380  stoweidlem55  46407  stoweid  46415  stirlinglem5  46430  stirlinglem12  46437  dirkerper  46448  dirkertrigeqlem3  46452  dirkertrigeq  46453  dirkercncflem1  46455  dirkercncflem2  46456  dirkercncf  46459  fourierdlem10  46469  fourierdlem12  46471  fourierdlem24  46483  fourierdlem30  46489  fourierdlem31  46490  fourierdlem32  46491  fourierdlem33  46492  fourierdlem34  46493  fourierdlem35  46494  fourierdlem37  46496  fourierdlem40  46499  fourierdlem41  46500  fourierdlem42  46501  fourierdlem43  46502  fourierdlem44  46503  fourierdlem46  46504  fourierdlem48  46506  fourierdlem49  46507  fourierdlem51  46509  fourierdlem54  46512  fourierdlem62  46520  fourierdlem64  46522  fourierdlem65  46523  fourierdlem70  46528  fourierdlem71  46529  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem78  46536  fourierdlem79  46537  fourierdlem80  46538  fourierdlem81  46539  fourierdlem82  46540  fourierdlem92  46550  fourierdlem93  46551  fourierdlem97  46555  fourierdlem101  46559  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem109  46567  fourierdlem114  46572  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  elaa2lem  46585  etransclem15  46601  etransclem19  46605  etransclem20  46606  etransclem22  46608  etransclem23  46609  etransclem24  46610  etransclem25  46611  etransclem27  46613  etransclem28  46614  etransclem35  46621  etransclem38  46624  qndenserrnbl  46647  ioorrnopn  46657  ioorrnopnxrlem  46658  ioorrnopnxr  46659  prsal  46670  salexct  46686  issalnnd  46697  sge0sn  46731  sge0tsms  46732  sge0cl  46733  sge0f1o  46734  sge0sup  46743  sge0less  46744  sge0pr  46746  sge0prle  46753  sge0le  46759  sge0split  46761  sge0splitmpt  46763  sge0iunmptlemfi  46765  sge0iunmpt  46770  sge0isum  46779  sge0xaddlem1  46785  sge0xadd  46787  sge0gtfsumgt  46795  nnfoctbdjlem  46807  iundjiun  46812  meadjun  46814  ismeannd  46819  voliunsge0lem  46824  meaiuninc3v  46836  caragenfiiuncl  46867  omeiunltfirp  46871  carageniuncl  46875  caragenunicl  46876  isomenndlem  46882  isomennd  46883  hoicvr  46900  ovnssle  46913  ovn0  46918  ovnsubadd  46924  hsphoidmvle2  46937  hoidmvval0b  46942  hoidmv1lelem1  46943  hoidmv1lelem2  46944  hoidmv1le  46946  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem5  46951  hoidmvle  46952  ovnhoilem1  46953  ovnhoi  46955  ovnlecvr2  46962  hspdifhsp  46968  hoidifhspdmvle  46972  hoiqssbl  46977  hspmbllem1  46978  hspmbllem2  46979  hspmbl  46981  hoimbl  46983  volico2  46993  ovolval2lem  46995  ovnsubadd2lem  46997  ovolval4lem1  47001  ovolval4lem2  47002  ovolval5lem1  47004  vonhoire  47024  iunhoiioo  47028  vonioo  47034  vonicc  47037  vonsn  47043  pimrecltpos  47060  incsmflem  47093  smfpimltxr  47099  smfconst  47101  decsmflem  47118  smfpimgtxr  47132  smfrec  47141  smfpimne2  47192  sharhght  47217  rrx2linest  49096  mofsn2  49198  ipolub00  49346  resccat  49427  initopropdlemlem  49592  prcof1  49741