Theorem pm2.61dan 818

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 413	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61dan.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
4	3	ex 413	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
5	2, 4	pm2.61d 180	1 ⊢ (𝜑 → 𝜒)

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

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 208  df-an 397

This theorem is referenced by:  pm2.61ddan  819  pm2.61dda  820  nfsb4t  2507  sbal2  2537  pm2.61danel  3053  ifeq1da  4493  ifeq2da  4494  ifeq12da  4495  ifclda  4497  ifeqda  4498  ifbothda  4500  2if2  4517  somin1  6090  xpcan  6134  fvmpti  6941  fvmptss  6955  funressn  7109  ovima0  7542  ordsuci  7758  suppssov1  8144  suppssov2  8145  oeoa  8530  oeoe  8532  omabs  8584  eceqoveq  8766  domdifsn  8995  pw2f1olem  9016  mapdom1  9077  imafiOLD  9223  marypha1lem  9343  supval2  9365  infdifsn  9576  ttrcltr  9635  ttrclselem1  9644  carden2b  9889  fidomtri  9915  dfac12lem2  10065  infunsdom1  10132  infunsdom  10133  itunisuc  10339  gchdomtri  10550  fiminre2  12102  xrmax2  13126  xrmin1  13127  ifle  13147  xnn0lem1lt  13194  xmulneg1  13219  xrsupsslem  13257  xrinfmsslem  13258  fzneuz  13560  seqf1olem1  14001  bccmpl  14269  bcval5  14278  bcpasc  14281  bccl  14282  hasheni  14308  hashfn  14335  hashdom  14339  hashdomi  14340  hashge1  14349  hashbc  14413  pfxval0  14637  sumz  15682  sumss  15684  fsumsplitsn  15704  sumsplit  15728  prod1  15907  prodss  15910  fprodsplitsn  15952  fprodle  15959  bitsmod  16403  sadadd2lem2  16417  sadcaddlem  16424  gcddvds  16470  gcdcl  16473  gcdneg  16489  dvdslcm  16565  lcmcl  16568  lcmneg  16570  lcmgcd  16574  lcmfcl  16595  dvdslcmf  16598  pcgcd  16847  pcmpt  16861  pcmpt2  16862  pcprod  16864  fldivp1  16866  prmreclem4  16888  vdwlem6  16955  ramub1lem1  16995  cidpropd  17674  rescabs  17798  lubval  18318  glbval  18331  joinval  18339  meetval  18353  acsexdimd  18523  gsumpropd2lem  18645  gsumval2  18652  mulgfval  19043  f1otrspeq  19420  pmtrfinv  19434  psgnunilem1  19466  gsumval3  19880  ablfac1c  20046  ablfac1eu  20048  mgpress  20129  orngsqr  20845  frlmsslsp  21778  psrbas  21916  resspsrbas  21955  mplmonmul  22019  mplcoe1  22020  mplcoe5  22023  opsrle  22030  opsrbaslem  22032  psrbaspropd  22226  mplbaspropd  22228  mdetdiag  22589  mdetunilem7  22608  mdetunilem9  22610  maducoeval2  22630  madurid  22634  opnnei  23110  restbas  23148  hauspwdom  23491  ptcmplem5  24046  xrsmopn  24803  xrhmeo  24938  lebnum  24956  pcoass  25016  pcorevlem  25018  icombl  25556  ioombl  25557  mbfconstlem  25619  mbfima  25622  i1fd  25673  mbfi1fseqlem5  25711  itg2const2  25733  itg2seq  25734  itg2uba  25735  itg2splitlem  25740  itg2split  25741  itg2monolem1  25742  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  iblss  25797  iblss2  25798  itgss  25804  bddmulibl  25831  coemullem  26240  aaliou2b  26332  isppw2  27103  mule1  27136  ppip1le  27149  dchrelbas3  27226  dchrpt  27255  bposlem3  27274  bposlem5  27276  bposlem6  27277  lgslem4  27288  lgsneg  27309  lgsmod  27311  lgsdilem  27312  lgsdir  27320  lgsdi  27322  lgsne0  27323  lgsquad3  27375  dchrvmasum2if  27485  maxs2  27759  mins1  27760  z12bday  28502  midexlem  28785  colperpex  28826  outpasch  28848  hlpasch  28849  lnopp2hpgb  28856  lmieu  28877  inaghl  28938  cgrg3col4  28946  pthdlem1  29859  nmcfnlbi  32148  elpreq  32623  prssad  32624  prssbd  32625  disjdifprg  32671  disjun0  32691  argcj  32847  f1ocnt  32899  xrge0npcan  33106  psgnfzto1stlem  33188  cyc3genpmlem  33239  cyc3conja  33245  archiabl  33286  erlval  33346  1arithufdlem3  33636  1arithufd  33638  psrmonmul  33741  esplyfval3  33763  resssra  33778  lbslelsp  33789  constrrecl  33960  constrinvcl  33964  constrsqrtcl  33970  1smat1  33995  esumcst  34254  esumrnmpt2  34259  hasheuni  34276  esumcvg  34277  ddemeas  34427  omssubadd  34491  eulerpartlemgc  34553  eulerpartlemb  34559  plymulx  34739  signswmnd  34748  fineqvnttrclselem1  35309  pthhashvtx  35363  erdsze2lem1  35438  mrsubvrs  35757  unblimceq0lem  36819  unbdqndv2lem2  36823  knoppndvlem10  36834  wl-spae  37899  wl-cbvalnaed  37910  wl-nfeqfb  37914  unccur  37977  poimirlem15  38009  poimirlem22  38016  itg2addnclem  38045  itg2addnclem2  38046  iblmulc2nc  38059  ftc1anclem5  38071  ftc1anc  38075  dvasin  38078  areacirclem5  38086  exmid2  38473  3dim1  39966  3dim2  39967  3dim3  39968  3atlem3  39984  3atlem7  39988  lvolnle3at  40081  2lplnja  40118  paddasslem18  40336  lhpexle3lem  40510  4atex  40575  cdlemd5  40701  cdleme16  40784  cdleme20  40823  cdleme21j  40835  cdleme21  40836  cdleme32snaw  40934  cdleme32fvcl  40939  cdleme32le  40946  cdlemeg46gf  41032  cdleme48gfv  41036  cdleme50trn12  41051  cdlemg6  41122  cdlemg7N  41125  cdlemg38  41214  cdlemg46  41234  dibvalrel  41662  dihlss  41749  dihglblem5aN  41791  dihmeetbN  41802  dihmeetALTN  41826  dihatlat  41833  dihatexv  41837  dvh3dim2  41947  dvh3dim3N  41948  lclkrlem2h  42013  mapdh8d  42282  mapdh8g  42284  hdmap11lem2  42341  lcmineqlem23  42543  aks4d1p3  42570  aks4d1p5  42572  aks4d1p7d1  42574  posbezout  42592  aks6d1c2p2  42611  aks6d1c4  42616  aks6d1c5lem1  42628  aks6d1c6lem3  42664  aks6d1c6lem4  42665  bcled  42670  bcle2d  42671  aks6d1c7  42676  grpods  42686  unitscyglem2  42688  unitscyglem4  42690  aks5lem8  42693  dffltz  43091  ttac  43488  pw2f1ocnv  43489  aomclem5  43510  isnumbasgrplem3  43557  iocmbl  43665  oe0suclim  43729  tfsconcatfv  43793  safesnsupfidom1o  43868  safesnsupfilb  43869  r1rankcld  44682  grur1cld  44683  grucollcld  44711  mnuprd  44727  radcnvrat  44765  bccbc  44796  binomcxp  44808  fnchoice  45484  fiiuncl  45520  eliin2f  45558  founiiun0  45644  axccdom  45674  axccd2  45681  fzisoeu  45755  fperiodmul  45759  upbdrech2  45763  fzdifsuc2  45765  uzfissfz  45778  supxrgere  45785  supxrgelem  45789  supxrge  45790  suplesup  45791  infrpge  45803  xrlexaddrp  45804  xralrple2  45806  infxr  45818  infleinflem1  45821  infleinflem2  45822  infleinf  45823  xralrple3  45825  xrralrecnnge  45841  uzublem  45880  supxrmnf2  45883  infxrpnf  45896  infxrpnf2  45913  supminfxr  45914  supminfxr2  45919  pimxrneun  45938  rexanuz2nf  45942  ioondisj2  45945  iccdifprioo  45968  fmul01lt1lem1  46036  fmul01lt1lem2  46037  limciccioolb  46073  lptioo2  46083  lptioo1  46084  limcicciooub  46087  lptre2pt  46090  limcresiooub  46092  limcresioolb  46093  limcleqr  46094  climfveq  46119  climfveqf  46130  limsupubuzlem  46162  limsupubuz  46163  limsupmnfuzlem  46176  limsupre3uzlem  46185  climxrre  46200  limsup10exlem  46222  cnrefiisplem  46279  climxlim2lem  46295  dfxlim2v  46297  xlimliminflimsup  46312  coskpi2  46316  cosknegpi  46319  icccncfext  46337  cncfiooicclem1  46343  cncfiooicc  46344  cncfiooiccre  46345  dvbdfbdioolem2  46379  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnxpaek  46392  dvnprodlem1  46396  dvnprodlem3  46398  volioc  46422  itgioocnicc  46427  iblcncfioo  46428  volico  46433  sublevolico  46434  ismbl3  46436  ovolsplit  46438  volioore  46440  voliooico  46442  voliccico  46449  stoweidlem14  46464  stoweidlem26  46476  stoweidlem28  46478  stoweidlem55  46505  stoweid  46513  stirlinglem5  46528  stirlinglem12  46535  dirkerper  46546  dirkertrigeqlem3  46550  dirkertrigeq  46551  dirkercncflem1  46553  dirkercncflem2  46554  dirkercncf  46557  fourierdlem10  46567  fourierdlem12  46569  fourierdlem24  46581  fourierdlem30  46587  fourierdlem31  46588  fourierdlem32  46589  fourierdlem33  46590  fourierdlem34  46591  fourierdlem35  46592  fourierdlem37  46594  fourierdlem40  46597  fourierdlem41  46598  fourierdlem42  46599  fourierdlem43  46600  fourierdlem44  46601  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem51  46607  fourierdlem54  46610  fourierdlem62  46618  fourierdlem64  46620  fourierdlem65  46621  fourierdlem70  46626  fourierdlem71  46627  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem78  46634  fourierdlem79  46635  fourierdlem80  46636  fourierdlem81  46637  fourierdlem82  46638  fourierdlem92  46648  fourierdlem93  46649  fourierdlem97  46653  fourierdlem101  46657  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem109  46665  fourierdlem114  46670  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  elaa2lem  46683  etransclem15  46699  etransclem19  46703  etransclem20  46704  etransclem22  46706  etransclem23  46707  etransclem24  46708  etransclem25  46709  etransclem27  46711  etransclem28  46712  etransclem35  46719  etransclem38  46722  qndenserrnbl  46745  ioorrnopn  46755  ioorrnopnxrlem  46756  ioorrnopnxr  46757  prsal  46768  salexct  46784  issalnnd  46795  sge0sn  46829  sge0tsms  46830  sge0cl  46831  sge0f1o  46832  sge0sup  46841  sge0less  46842  sge0pr  46844  sge0prle  46851  sge0le  46857  sge0split  46859  sge0splitmpt  46861  sge0iunmptlemfi  46863  sge0iunmpt  46868  sge0isum  46877  sge0xaddlem1  46883  sge0xadd  46885  sge0gtfsumgt  46893  nnfoctbdjlem  46905  iundjiun  46910  meadjun  46912  ismeannd  46917  voliunsge0lem  46922  meaiuninc3v  46934  caragenfiiuncl  46965  omeiunltfirp  46969  carageniuncl  46973  caragenunicl  46974  isomenndlem  46980  isomennd  46981  hoicvr  46998  ovnssle  47011  ovn0  47016  ovnsubadd  47022  hsphoidmvle2  47035  hoidmvval0b  47040  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1le  47044  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem5  47049  hoidmvle  47050  ovnhoilem1  47051  ovnhoi  47053  ovnlecvr2  47060  hspdifhsp  47066  hoidifhspdmvle  47070  hoiqssbl  47075  hspmbllem1  47076  hspmbllem2  47077  hspmbl  47079  hoimbl  47081  volico2  47091  ovolval2lem  47093  ovnsubadd2lem  47095  ovolval4lem1  47099  ovolval4lem2  47100  ovolval5lem1  47102  vonhoire  47122  iunhoiioo  47126  vonioo  47132  vonicc  47135  vonsn  47141  pimrecltpos  47158  incsmflem  47191  smfpimltxr  47197  smfconst  47199  decsmflem  47216  smfpimgtxr  47230  smfrec  47239  smfpimne2  47290  sharhght  47315  rrx2linest  49240  mofsn2  49342  ipolub00  49490  resccat  49571  initopropdlemlem  49736  prcof1  49885