Theorem pm2.61dan 812

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  813  pm2.61dda  814  nfsb4t  2503  sbal2  2533  pm2.61danel  3050  ifeq1da  4511  ifeq2da  4512  ifeq12da  4513  ifclda  4515  ifeqda  4516  ifbothda  4518  2if2  4535  somin1  6090  xpcan  6134  fvmpti  6940  fvmptss  6953  funressn  7104  ovima0  7537  ordsuci  7753  suppssov1  8139  suppssov2  8140  oeoa  8525  oeoe  8527  omabs  8579  eceqoveq  8759  domdifsn  8988  pw2f1olem  9009  mapdom1  9070  imafiOLD  9216  marypha1lem  9336  supval2  9358  infdifsn  9566  ttrcltr  9625  ttrclselem1  9634  carden2b  9879  fidomtri  9905  dfac12lem2  10055  infunsdom1  10122  infunsdom  10123  itunisuc  10329  gchdomtri  10540  fiminre2  12090  xrmax2  13091  xrmin1  13092  ifle  13112  xnn0lem1lt  13159  xmulneg1  13184  xrsupsslem  13222  xrinfmsslem  13223  fzneuz  13524  seqf1olem1  13964  bccmpl  14232  bcval5  14241  bcpasc  14244  bccl  14245  hasheni  14271  hashfn  14298  hashdom  14302  hashdomi  14303  hashge1  14312  hashbc  14376  pfxval0  14600  sumz  15645  sumss  15647  fsumsplitsn  15667  sumsplit  15691  prod1  15867  prodss  15870  fprodsplitsn  15912  fprodle  15919  bitsmod  16363  sadadd2lem2  16377  sadcaddlem  16384  gcddvds  16430  gcdcl  16433  gcdneg  16449  dvdslcm  16525  lcmcl  16528  lcmneg  16530  lcmgcd  16534  lcmfcl  16555  dvdslcmf  16558  pcgcd  16806  pcmpt  16820  pcmpt2  16821  pcprod  16823  fldivp1  16825  prmreclem4  16847  vdwlem6  16914  ramub1lem1  16954  cidpropd  17633  rescabs  17757  lubval  18277  glbval  18290  joinval  18298  meetval  18312  acsexdimd  18482  gsumpropd2lem  18604  gsumval2  18611  mulgfval  18999  f1otrspeq  19376  pmtrfinv  19390  psgnunilem1  19422  gsumval3  19836  ablfac1c  20002  ablfac1eu  20004  mgpress  20085  orngsqr  20799  frlmsslsp  21751  psrbas  21889  resspsrbas  21929  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  opsrle  22002  opsrbaslem  22004  psrbaspropd  22175  mplbaspropd  22177  mdetdiag  22543  mdetunilem7  22562  mdetunilem9  22564  maducoeval2  22584  madurid  22588  opnnei  23064  restbas  23102  hauspwdom  23445  ptcmplem5  24000  xrsmopn  24757  xrhmeo  24900  lebnum  24919  pcoass  24980  pcorevlem  24982  icombl  25521  ioombl  25522  mbfconstlem  25584  mbfima  25587  i1fd  25638  mbfi1fseqlem5  25676  itg2const2  25698  itg2seq  25699  itg2uba  25700  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  iblss  25762  iblss2  25763  itgss  25769  bddmulibl  25796  coemullem  26211  aaliou2b  26305  isppw2  27081  mule1  27114  ppip1le  27127  dchrelbas3  27205  dchrpt  27234  bposlem3  27253  bposlem5  27255  bposlem6  27256  lgslem4  27267  lgsneg  27288  lgsmod  27290  lgsdilem  27291  lgsdir  27299  lgsdi  27301  lgsne0  27302  lgsquad3  27354  dchrvmasum2if  27464  maxs2  27738  mins1  27739  z12bday  28481  midexlem  28764  colperpex  28805  outpasch  28827  hlpasch  28828  lnopp2hpgb  28835  lmieu  28856  inaghl  28917  cgrg3col4  28925  pthdlem1  29839  nmcfnlbi  32127  elpreq  32603  prssad  32604  prssbd  32605  disjdifprg  32650  disjun0  32670  argcj  32828  f1ocnt  32880  xrge0npcan  33102  psgnfzto1stlem  33182  cyc3genpmlem  33233  cyc3conja  33239  archiabl  33280  erlval  33340  1arithufdlem3  33627  1arithufd  33629  esplyfval3  33730  resssra  33743  lbslelsp  33754  constrrecl  33926  constrinvcl  33930  constrsqrtcl  33936  1smat1  33961  esumcst  34220  esumrnmpt2  34225  hasheuni  34242  esumcvg  34243  ddemeas  34393  omssubadd  34457  eulerpartlemgc  34519  eulerpartlemb  34525  plymulx  34705  signswmnd  34714  fineqvnttrclselem1  35277  pthhashvtx  35322  erdsze2lem1  35397  mrsubvrs  35716  unblimceq0lem  36706  unbdqndv2lem2  36710  knoppndvlem10  36721  wl-spae  37722  wl-cbvalnaed  37733  wl-nfeqfb  37737  unccur  37800  poimirlem15  37832  poimirlem22  37839  itg2addnclem  37868  itg2addnclem2  37869  iblmulc2nc  37882  ftc1anclem5  37894  ftc1anc  37898  dvasin  37901  areacirclem5  37909  exmid2  38296  3dim1  39723  3dim2  39724  3dim3  39725  3atlem3  39741  3atlem7  39745  lvolnle3at  39838  2lplnja  39875  paddasslem18  40093  lhpexle3lem  40267  4atex  40332  cdlemd5  40458  cdleme16  40541  cdleme20  40580  cdleme21j  40592  cdleme21  40593  cdleme32snaw  40691  cdleme32fvcl  40696  cdleme32le  40703  cdlemeg46gf  40789  cdleme48gfv  40793  cdleme50trn12  40808  cdlemg6  40879  cdlemg7N  40882  cdlemg38  40971  cdlemg46  40991  dibvalrel  41419  dihlss  41506  dihglblem5aN  41548  dihmeetbN  41559  dihmeetALTN  41583  dihatlat  41590  dihatexv  41594  dvh3dim2  41704  dvh3dim3N  41705  lclkrlem2h  41770  mapdh8d  42039  mapdh8g  42041  hdmap11lem2  42098  lcmineqlem23  42301  aks4d1p3  42328  aks4d1p5  42330  aks4d1p7d1  42332  posbezout  42350  aks6d1c2p2  42369  aks6d1c4  42374  aks6d1c5lem1  42386  aks6d1c6lem3  42422  aks6d1c6lem4  42423  bcled  42428  bcle2d  42429  aks6d1c7  42434  grpods  42444  unitscyglem2  42446  unitscyglem4  42448  aks5lem8  42451  dffltz  42873  ttac  43274  pw2f1ocnv  43275  aomclem5  43296  isnumbasgrplem3  43343  iocmbl  43451  oe0suclim  43515  tfsconcatfv  43579  safesnsupfidom1o  43654  safesnsupfilb  43655  r1rankcld  44468  grur1cld  44469  grucollcld  44497  mnuprd  44513  radcnvrat  44551  bccbc  44582  binomcxp  44594  fnchoice  45270  fiiuncl  45306  eliin2f  45344  founiiun0  45430  axccdom  45462  axccd2  45470  fzisoeu  45544  fperiodmul  45548  upbdrech2  45552  fzdifsuc2  45554  uzfissfz  45567  supxrgere  45574  supxrgelem  45578  supxrge  45579  suplesup  45580  infrpge  45592  xrlexaddrp  45593  xralrple2  45595  infxr  45607  infleinflem1  45610  infleinflem2  45611  infleinf  45612  xralrple3  45614  xrralrecnnge  45630  uzublem  45670  supxrmnf2  45673  infxrpnf  45686  infxrpnf2  45703  supminfxr  45704  supminfxr2  45709  pimxrneun  45728  rexanuz2nf  45732  ioondisj2  45735  iccdifprioo  45758  fmul01lt1lem1  45826  fmul01lt1lem2  45827  limciccioolb  45863  lptioo2  45873  lptioo1  45874  limcicciooub  45877  lptre2pt  45880  limcresiooub  45882  limcresioolb  45883  limcleqr  45884  climfveq  45909  climfveqf  45920  limsupubuzlem  45952  limsupubuz  45953  limsupmnfuzlem  45966  limsupre3uzlem  45975  climxrre  45990  limsup10exlem  46012  cnrefiisplem  46069  climxlim2lem  46085  dfxlim2v  46087  xlimliminflimsup  46102  coskpi2  46106  cosknegpi  46109  icccncfext  46127  cncfiooicclem1  46133  cncfiooicc  46134  cncfiooiccre  46135  dvbdfbdioolem2  46169  ioodvbdlimc1lem1  46171  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnxpaek  46182  dvnprodlem1  46186  dvnprodlem3  46188  volioc  46212  itgioocnicc  46217  iblcncfioo  46218  volico  46223  sublevolico  46224  ismbl3  46226  ovolsplit  46228  volioore  46230  voliooico  46232  voliccico  46239  stoweidlem14  46254  stoweidlem26  46266  stoweidlem28  46268  stoweidlem55  46295  stoweid  46303  stirlinglem5  46318  stirlinglem12  46325  dirkerper  46336  dirkertrigeqlem3  46340  dirkertrigeq  46341  dirkercncflem1  46343  dirkercncflem2  46344  dirkercncf  46347  fourierdlem10  46357  fourierdlem12  46359  fourierdlem24  46371  fourierdlem30  46377  fourierdlem31  46378  fourierdlem32  46379  fourierdlem33  46380  fourierdlem34  46381  fourierdlem35  46382  fourierdlem37  46384  fourierdlem40  46387  fourierdlem41  46388  fourierdlem42  46389  fourierdlem43  46390  fourierdlem44  46391  fourierdlem46  46392  fourierdlem48  46394  fourierdlem49  46395  fourierdlem51  46397  fourierdlem54  46400  fourierdlem62  46408  fourierdlem64  46410  fourierdlem65  46411  fourierdlem70  46416  fourierdlem71  46417  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem78  46424  fourierdlem79  46425  fourierdlem80  46426  fourierdlem81  46427  fourierdlem82  46428  fourierdlem92  46438  fourierdlem93  46439  fourierdlem97  46443  fourierdlem101  46447  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem109  46455  fourierdlem114  46460  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  elaa2lem  46473  etransclem15  46489  etransclem19  46493  etransclem20  46494  etransclem22  46496  etransclem23  46497  etransclem24  46498  etransclem25  46499  etransclem27  46501  etransclem28  46502  etransclem35  46509  etransclem38  46512  qndenserrnbl  46535  ioorrnopn  46545  ioorrnopnxrlem  46546  ioorrnopnxr  46547  prsal  46558  salexct  46574  issalnnd  46585  sge0sn  46619  sge0tsms  46620  sge0cl  46621  sge0f1o  46622  sge0sup  46631  sge0less  46632  sge0pr  46634  sge0prle  46641  sge0le  46647  sge0split  46649  sge0splitmpt  46651  sge0iunmptlemfi  46653  sge0iunmpt  46658  sge0isum  46667  sge0xaddlem1  46673  sge0xadd  46675  sge0gtfsumgt  46683  nnfoctbdjlem  46695  iundjiun  46700  meadjun  46702  ismeannd  46707  voliunsge0lem  46712  meaiuninc3v  46724  caragenfiiuncl  46755  omeiunltfirp  46759  carageniuncl  46763  caragenunicl  46764  isomenndlem  46770  isomennd  46771  hoicvr  46788  ovnssle  46801  ovn0  46806  ovnsubadd  46812  hsphoidmvle2  46825  hoidmvval0b  46830  hoidmv1lelem1  46831  hoidmv1lelem2  46832  hoidmv1le  46834  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem5  46839  hoidmvle  46840  ovnhoilem1  46841  ovnhoi  46843  ovnlecvr2  46850  hspdifhsp  46856  hoidifhspdmvle  46860  hoiqssbl  46865  hspmbllem1  46866  hspmbllem2  46867  hspmbl  46869  hoimbl  46871  volico2  46881  ovolval2lem  46883  ovnsubadd2lem  46885  ovolval4lem1  46889  ovolval4lem2  46890  ovolval5lem1  46892  vonhoire  46912  iunhoiioo  46916  vonioo  46922  vonicc  46925  vonsn  46931  pimrecltpos  46948  incsmflem  46981  smfpimltxr  46987  smfconst  46989  decsmflem  47006  smfpimgtxr  47020  smfrec  47029  smfpimne2  47080  sharhght  47105  rrx2linest  48984  mofsn2  49086  ipolub00  49234  resccat  49315  initopropdlemlem  49480  prcof1  49629