Theorem pm2.61dan 825

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm2.61ddan  826  pm2.61dda  827  nfsb4t  2528  sbal2  2558  pm2.61danel  3075  ifeq1da  4514  ifeq2da  4515  ifeq12da  4516  ifclda  4518  ifeqda  4519  ifbothda  4521  2if2  4538  somin1  6127  xpcan  6169  fvmpti  6985  fvmptss  6999  funressn  7156  ovima0  7593  ordsuci  7807  suppssov1  8195  suppssov2  8196  oeoa  8585  oeoe  8587  omabs  8639  eceqoveq  8822  domdifsn  9058  pw2f1olem  9079  mapdom1  9140  marypha1lem  9403  supval2  9425  infdifsn  9636  ttrcltr  9695  ttrclselem1  9704  carden2b  9972  fidomtri  9998  dfac12lem2  10147  infunsdom1  10214  infunsdom  10215  itunisuc  10421  gchdomtri  10638  fiminre2  12187  xrmax2  13228  xrmin1  13229  ifle  13249  xnn0lem1lt  13296  xmulneg1  13321  xrsupsslem  13359  xrinfmsslem  13360  fzneuz  13663  seqf1olem1  14105  bccmpl  14373  bcval5  14382  bcpasc  14385  bccl  14386  hasheni  14412  hashfn  14439  hashdom  14443  hashdomi  14444  hashge1  14453  hashbc  14518  pfxval0  14746  sumz  15808  sumss  15810  fsumsplitsn  15830  sumsplit  15854  prod1  16031  prodss  16034  fprodsplitsn  16076  fprodle  16083  bitsmod  16526  sadadd2lem2  16540  sadcaddlem  16547  gcddvds  16593  gcdcl  16596  gcdneg  16612  dvdslcm  16688  lcmcl  16691  lcmneg  16693  lcmgcd  16697  lcmfcl  16718  dvdslcmf  16721  pcgcd  16970  pcmpt  16984  pcmpt2  16985  pcprod  16987  fldivp1  16989  prmreclem4  17011  vdwlem6  17078  ramub1lem1  17118  cidpropd  17798  rescabs  17922  lubval  18442  glbval  18455  joinval  18463  meetval  18477  acsexdimd  18647  gsumpropd2lem  18781  gsumval2  18788  mulgfval  19192  f1otrspeq  19574  pmtrfinv  19588  psgnunilem1  19620  gsumval3  20034  ablfac1c  20200  ablfac1eu  20202  mgpress  20283  orngsqr  21032  frlmsslsp  22009  psrbas  22149  resspsrbas  22188  mplmonmul  22252  mplcoe1  22253  mplcoe5  22256  opsrle  22263  opsrbaslem  22265  psrbaspropd  22459  mplbaspropd  22461  mdetdiag  22821  mdetunilem7  22840  mdetunilem9  22842  maducoeval2  22862  madurid  22866  opnnei  23345  restbas  23383  hauspwdom  23727  ptcmplem5  24282  xrsmopn  25039  xrhmeo  25174  lebnum  25192  pcoass  25252  pcorevlem  25254  icombl  25792  ioombl  25793  mbfconstlem  25855  mbfima  25858  i1fd  25909  mbfi1fseqlem5  25947  itg2const2  25969  itg2seq  25970  itg2uba  25971  itg2splitlem  25976  itg2split  25977  itg2monolem1  25978  itg2gt0  25988  itg2cnlem1  25989  itg2cnlem2  25990  iblss  26032  iblss2  26033  itgss  26039  bddmulibl  26066  coemullem  26476  plymulidp  26512  aaliou2b  26577  isppw2  27351  mule1  27384  ppip1le  27397  dchrelbas3  27474  dchrpt  27503  bposlem3  27522  bposlem5  27524  bposlem6  27525  lgslem4  27536  lgsneg  27557  lgsmod  27559  lgsdilem  27560  lgsdir  27568  lgsdi  27570  lgsne0  27571  lgsquad3  27623  dchrvmasum2if  27733  maxs2  28006  mins1  28007  z12bday  28750  tglnpt4  29002  midexlem  29043  colperpex  29088  outpasch  29112  hlpasch  29113  lnopp2hpgb  29120  lmieu  29168  perpeq  29227  tgaaddcpbl  29231  inaghl  29243  cgrg3col4  29251  angmgmaddov1lem  29265  angmgmaddrid  29272  perpprlng  29307  prlngex  29308  prlngmo2  29313  pthhashvtx  30194  pthdlem1  30231  nmcfnlbi  32533  elpreq  33003  prssad  33004  prssbd  33005  disjdifprg  33048  disjun0  33068  argcj  33219  f1ocnt  33271  xrge0npcan  33460  psgnfzto1stlem  33540  cyc3genpmlem  33591  cyc3conja  33597  archiabl  33638  erlval  33698  1arithufdlem3  33956  1arithufd  33958  psrmonmul  34060  esplyfval3  34082  resssra  34097  lbslelsp  34108  constrrecl  34279  constrinvcl  34283  constrsqrtcl  34289  1smat1  34314  esumcst  34573  esumrnmpt2  34578  hasheuni  34595  esumcvg  34596  ddemeas  34747  omssubadd  34811  eulerpartlemgc  34873  eulerpartlemb  34879  signswmnd  35065  fineqvnttrclselem1  35647  erdsze2lem1  35782  mrsubvrs  36101  unblimceq0lem  37203  unbdqndv2lem2  37207  knoppndvlem10  37218  wl-spae  38284  wl-cbvalnaed  38295  wl-nfeqfb  38299  unccur  38357  poimirlem15  38384  poimirlem22  38391  itg2addnclem  38420  itg2addnclem2  38421  iblmulc2nc  38434  ftc1anclem5  38446  ftc1anc  38450  dvasin  38453  areacirclem5  38461  exmid2  38847  3dim1  40340  3dim2  40341  3dim3  40342  3atlem3  40358  3atlem7  40362  lvolnle3at  40455  2lplnja  40492  paddasslem18  40710  lhpexle3lem  40884  4atex  40949  cdlemd5  41075  cdleme16  41158  cdleme20  41197  cdleme21j  41209  cdleme21  41210  cdleme32snaw  41308  cdleme32fvcl  41313  cdleme32le  41320  cdlemeg46gf  41406  cdleme48gfv  41410  cdleme50trn12  41425  cdlemg6  41496  cdlemg7N  41499  cdlemg38  41588  cdlemg46  41608  dibvalrel  42036  dihlss  42123  dihglblem5aN  42165  dihmeetbN  42176  dihmeetALTN  42200  dihatlat  42207  dihatexv  42211  dvh3dim2  42321  dvh3dim3N  42322  lclkrlem2h  42387  mapdh8d  42656  mapdh8g  42658  hdmap11lem2  42715  lcmineqlem23  42917  aks4d1p3  42944  aks4d1p5  42946  aks4d1p7d1  42948  posbezout  42966  aks6d1c2p2  42985  aks6d1c4  42990  aks6d1c5lem1  43002  aks6d1c6lem3  43038  aks6d1c6lem4  43039  bcled  43044  bcle2d  43045  aks6d1c7  43050  grpods  43060  unitscyglem2  43062  unitscyglem4  43064  aks5lem8  43067  dffltz  43480  ttac  43877  pw2f1ocnv  43878  aomclem5  43899  isnumbasgrplem3  43946  iocmbl  44054  oe0suclim  44118  tfsconcatfv  44182  safesnsupfidom1o  44257  safesnsupfilb  44258  r1rankcld  45069  grur1cld  45070  grucollcld  45084  mnuprd  45100  radcnvrat  45138  bccbc  45169  binomcxp  45181  fnchoice  45863  fiiuncl  45899  eliin2f  45936  founiiun0  46022  axccdom  46052  axccd2  46059  fzisoeu  46133  fperiodmul  46137  upbdrech2  46141  fzdifsuc2  46143  uzfissfz  46156  supxrgere  46163  supxrgelem  46167  supxrge  46168  suplesup  46169  infrpge  46181  xrlexaddrp  46182  xralrple2  46184  infxr  46196  infleinflem1  46199  infleinflem2  46200  infleinf  46201  xralrple3  46203  xrralrecnnge  46219  uzublem  46258  supxrmnf2  46261  infxrpnf  46274  infxrpnf2  46291  supminfxr  46292  supminfxr2  46297  pimxrneun  46316  rexanuz2nf  46320  ioondisj2  46323  iccdifprioo  46346  fmul01lt1lem1  46414  fmul01lt1lem2  46415  limciccioolb  46451  lptioo2  46461  lptioo1  46462  limcicciooub  46465  lptre2pt  46468  limcresiooub  46470  limcresioolb  46471  limcleqr  46472  climfveq  46497  climfveqf  46508  limsupubuzlem  46540  limsupubuz  46541  limsupmnfuzlem  46554  limsupre3uzlem  46563  climxrre  46578  limsup10exlem  46600  cnrefiisplem  46657  climxlim2lem  46673  dfxlim2v  46675  xlimliminflimsup  46690  coskpi2  46694  cosknegpi  46697  icccncfext  46715  cncfiooicclem1  46721  cncfiooicc  46722  cncfiooiccre  46723  dvbdfbdioolem2  46757  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnxpaek  46770  dvnprodlem1  46774  dvnprodlem3  46776  volioc  46800  itgioocnicc  46805  iblcncfioo  46806  volico  46811  sublevolico  46812  ismbl3  46814  ovolsplit  46816  volioore  46818  voliooico  46820  voliccico  46827  stoweidlem14  46842  stoweidlem26  46854  stoweidlem28  46856  stoweidlem55  46883  stoweid  46891  stirlinglem5  46906  stirlinglem12  46913  dirkerper  46924  dirkertrigeqlem3  46928  dirkertrigeq  46929  dirkercncflem1  46931  dirkercncflem2  46932  dirkercncf  46935  fourierdlem10  46945  fourierdlem12  46947  fourierdlem24  46959  fourierdlem30  46965  fourierdlem31  46966  fourierdlem32  46967  fourierdlem33  46968  fourierdlem34  46969  fourierdlem35  46970  fourierdlem37  46972  fourierdlem40  46975  fourierdlem41  46976  fourierdlem42  46977  fourierdlem43  46978  fourierdlem44  46979  fourierdlem46  46980  fourierdlem48  46982  fourierdlem49  46983  fourierdlem51  46985  fourierdlem54  46988  fourierdlem62  46996  fourierdlem64  46998  fourierdlem65  46999  fourierdlem70  47004  fourierdlem71  47005  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem78  47012  fourierdlem79  47013  fourierdlem80  47014  fourierdlem81  47015  fourierdlem82  47016  fourierdlem92  47026  fourierdlem93  47027  fourierdlem97  47031  fourierdlem101  47035  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem109  47043  fourierdlem114  47048  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  elaa2lem  47061  etransclem15  47077  etransclem19  47081  etransclem20  47082  etransclem22  47084  etransclem23  47085  etransclem24  47086  etransclem25  47087  etransclem27  47089  etransclem28  47090  etransclem35  47097  etransclem38  47100  qndenserrnbl  47123  ioorrnopn  47133  ioorrnopnxrlem  47134  ioorrnopnxr  47135  prsal  47146  salexct  47162  issalnnd  47173  sge0sn  47207  sge0tsms  47208  sge0cl  47209  sge0f1o  47210  sge0sup  47219  sge0less  47220  sge0pr  47222  sge0prle  47229  sge0le  47235  sge0split  47237  sge0splitmpt  47239  sge0iunmptlemfi  47241  sge0iunmpt  47246  sge0isum  47255  sge0xaddlem1  47261  sge0xadd  47263  sge0gtfsumgt  47271  nnfoctbdjlem  47283  iundjiun  47288  meadjun  47290  ismeannd  47295  voliunsge0lem  47300  meaiuninc3v  47312  caragenfiiuncl  47343  omeiunltfirp  47347  carageniuncl  47351  caragenunicl  47352  isomenndlem  47358  isomennd  47359  hoicvr  47376  ovnssle  47389  ovn0  47394  ovnsubadd  47400  hsphoidmvle2  47413  hoidmvval0b  47418  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1le  47422  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvlelem5  47427  hoidmvle  47428  ovnhoilem1  47429  ovnhoi  47431  ovnlecvr2  47438  hspdifhsp  47444  hoidifhspdmvle  47448  hoiqssbl  47453  hspmbllem1  47454  hspmbllem2  47455  hspmbl  47457  hoimbl  47459  volico2  47469  ovolval2lem  47471  ovnsubadd2lem  47473  ovolval4lem1  47477  ovolval4lem2  47478  ovolval5lem1  47480  vonhoire  47500  iunhoiioo  47504  vonioo  47510  vonicc  47513  vonsn  47519  pimrecltpos  47536  incsmflem  47569  smfpimltxr  47575  smfconst  47577  decsmflem  47594  smfpimgtxr  47608  smfrec  47617  smfpimne2  47668  sharhght  47693  tmachlem-agreeprod  47765  rrx2linest  49672  mofsn2  49773  ipolub00  49919  resccat  50000  initopropdlemlem  50165  prcof1  50314