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  2499  sbal2  2529  pm2.61danel  3046  ifeq1da  4507  ifeq2da  4508  ifeq12da  4509  ifclda  4511  ifeqda  4512  ifbothda  4514  2if2  4531  somin1  6080  xpcan  6123  fvmpti  6928  fvmptss  6941  funressn  7092  ovima0  7525  ordsuci  7741  suppssov1  8127  suppssov2  8128  oeoa  8512  oeoe  8514  omabs  8566  eceqoveq  8746  domdifsn  8973  pw2f1olem  8994  mapdom1  9055  imafiOLD  9200  marypha1lem  9317  supval2  9339  infdifsn  9547  ttrcltr  9606  ttrclselem1  9615  carden2b  9857  fidomtri  9883  dfac12lem2  10033  infunsdom1  10100  infunsdom  10101  itunisuc  10307  gchdomtri  10517  fiminre2  12067  xrmax2  13072  xrmin1  13073  ifle  13093  xnn0lem1lt  13140  xmulneg1  13165  xrsupsslem  13203  xrinfmsslem  13204  fzneuz  13505  seqf1olem1  13945  bccmpl  14213  bcval5  14222  bcpasc  14225  bccl  14226  hasheni  14252  hashfn  14279  hashdom  14283  hashdomi  14284  hashge1  14293  hashbc  14357  pfxval0  14581  sumz  15626  sumss  15628  fsumsplitsn  15648  sumsplit  15672  prod1  15848  prodss  15851  fprodsplitsn  15893  fprodle  15900  bitsmod  16344  sadadd2lem2  16358  sadcaddlem  16365  gcddvds  16411  gcdcl  16414  gcdneg  16430  dvdslcm  16506  lcmcl  16509  lcmneg  16511  lcmgcd  16515  lcmfcl  16536  dvdslcmf  16539  pcgcd  16787  pcmpt  16801  pcmpt2  16802  pcprod  16804  fldivp1  16806  prmreclem4  16828  vdwlem6  16895  ramub1lem1  16935  cidpropd  17613  rescabs  17737  lubval  18257  glbval  18270  joinval  18278  meetval  18292  acsexdimd  18462  gsumpropd2lem  18584  gsumval2  18591  mulgfval  18979  f1otrspeq  19357  pmtrfinv  19371  psgnunilem1  19403  gsumval3  19817  ablfac1c  19983  ablfac1eu  19985  mgpress  20066  orngsqr  20779  frlmsslsp  21731  psrbas  21868  resspsrbas  21909  mplmonmul  21969  mplcoe1  21970  mplcoe5  21973  opsrle  21980  opsrbaslem  21982  psrbaspropd  22145  mplbaspropd  22147  mdetdiag  22512  mdetunilem7  22531  mdetunilem9  22533  maducoeval2  22553  madurid  22557  opnnei  23033  restbas  23071  hauspwdom  23414  ptcmplem5  23969  xrsmopn  24726  xrhmeo  24869  lebnum  24888  pcoass  24949  pcorevlem  24951  icombl  25490  ioombl  25491  mbfconstlem  25553  mbfima  25556  i1fd  25607  mbfi1fseqlem5  25645  itg2const2  25667  itg2seq  25668  itg2uba  25669  itg2splitlem  25674  itg2split  25675  itg2monolem1  25676  itg2gt0  25686  itg2cnlem1  25687  itg2cnlem2  25688  iblss  25731  iblss2  25732  itgss  25738  bddmulibl  25765  coemullem  26180  aaliou2b  26274  isppw2  27050  mule1  27083  ppip1le  27096  dchrelbas3  27174  dchrpt  27203  bposlem3  27222  bposlem5  27224  bposlem6  27225  lgslem4  27236  lgsneg  27257  lgsmod  27259  lgsdilem  27260  lgsdir  27268  lgsdi  27270  lgsne0  27271  lgsquad3  27323  dchrvmasum2if  27433  maxs2  27703  mins1  27704  midexlem  28668  colperpex  28709  outpasch  28731  hlpasch  28732  lnopp2hpgb  28739  lmieu  28760  inaghl  28821  cgrg3col4  28829  pthdlem1  29742  nmcfnlbi  32027  elpreq  32503  prssad  32504  prssbd  32505  disjdifprg  32550  disjun0  32570  argcj  32727  f1ocnt  32777  xrge0npcan  32996  psgnfzto1stlem  33064  cyc3genpmlem  33115  cyc3conja  33121  archiabl  33162  erlval  33220  1arithufdlem3  33506  1arithufd  33508  resssra  33594  lbslelsp  33605  constrrecl  33777  constrinvcl  33781  constrsqrtcl  33787  1smat1  33812  esumcst  34071  esumrnmpt2  34076  hasheuni  34093  esumcvg  34094  ddemeas  34244  omssubadd  34308  eulerpartlemgc  34370  eulerpartlemb  34376  plymulx  34556  signswmnd  34565  fineqvnttrclselem1  35129  pthhashvtx  35160  erdsze2lem1  35235  mrsubvrs  35554  unblimceq0lem  36539  unbdqndv2lem2  36543  knoppndvlem10  36554  wl-spae  37554  wl-cbvalnaed  37565  wl-nfeqfb  37569  unccur  37642  poimirlem15  37674  poimirlem22  37681  itg2addnclem  37710  itg2addnclem2  37711  iblmulc2nc  37724  ftc1anclem5  37736  ftc1anc  37740  dvasin  37743  areacirclem5  37751  exmid2  38138  3dim1  39505  3dim2  39506  3dim3  39507  3atlem3  39523  3atlem7  39527  lvolnle3at  39620  2lplnja  39657  paddasslem18  39875  lhpexle3lem  40049  4atex  40114  cdlemd5  40240  cdleme16  40323  cdleme20  40362  cdleme21j  40374  cdleme21  40375  cdleme32snaw  40473  cdleme32fvcl  40478  cdleme32le  40485  cdlemeg46gf  40571  cdleme48gfv  40575  cdleme50trn12  40590  cdlemg6  40661  cdlemg7N  40664  cdlemg38  40753  cdlemg46  40773  dibvalrel  41201  dihlss  41288  dihglblem5aN  41330  dihmeetbN  41341  dihmeetALTN  41365  dihatlat  41372  dihatexv  41376  dvh3dim2  41486  dvh3dim3N  41487  lclkrlem2h  41552  mapdh8d  41821  mapdh8g  41823  hdmap11lem2  41880  lcmineqlem23  42083  aks4d1p3  42110  aks4d1p5  42112  aks4d1p7d1  42114  posbezout  42132  aks6d1c2p2  42151  aks6d1c4  42156  aks6d1c5lem1  42168  aks6d1c6lem3  42204  aks6d1c6lem4  42205  bcled  42210  bcle2d  42211  aks6d1c7  42216  grpods  42226  unitscyglem2  42228  unitscyglem4  42230  aks5lem8  42233  dffltz  42666  ttac  43068  pw2f1ocnv  43069  aomclem5  43090  isnumbasgrplem3  43137  iocmbl  43245  oe0suclim  43309  tfsconcatfv  43373  safesnsupfidom1o  43449  safesnsupfilb  43450  r1rankcld  44263  grur1cld  44264  grucollcld  44292  mnuprd  44308  radcnvrat  44346  bccbc  44377  binomcxp  44389  fnchoice  45065  fiiuncl  45101  eliin2f  45140  founiiun0  45226  axccdom  45258  axccd2  45266  fzisoeu  45340  fperiodmul  45344  upbdrech2  45348  fzdifsuc2  45350  uzfissfz  45364  supxrgere  45371  supxrgelem  45375  supxrge  45376  suplesup  45377  infrpge  45389  xrlexaddrp  45390  xralrple2  45392  infxr  45404  infleinflem1  45407  infleinflem2  45408  infleinf  45409  xralrple3  45411  xrralrecnnge  45427  uzublem  45467  supxrmnf2  45470  infxrpnf  45483  infxrpnf2  45500  supminfxr  45501  supminfxr2  45506  pimxrneun  45525  rexanuz2nf  45529  ioondisj2  45532  iccdifprioo  45555  fmul01lt1lem1  45623  fmul01lt1lem2  45624  limciccioolb  45660  lptioo2  45670  lptioo1  45671  limcicciooub  45674  lptre2pt  45677  limcresiooub  45679  limcresioolb  45680  limcleqr  45681  climfveq  45706  climfveqf  45717  limsupubuzlem  45749  limsupubuz  45750  limsupmnfuzlem  45763  limsupre3uzlem  45772  climxrre  45787  limsup10exlem  45809  cnrefiisplem  45866  climxlim2lem  45882  dfxlim2v  45884  xlimliminflimsup  45899  coskpi2  45903  cosknegpi  45906  icccncfext  45924  cncfiooicclem1  45930  cncfiooicc  45931  cncfiooiccre  45932  dvbdfbdioolem2  45966  ioodvbdlimc1lem1  45968  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnxpaek  45979  dvnprodlem1  45983  dvnprodlem3  45985  volioc  46009  itgioocnicc  46014  iblcncfioo  46015  volico  46020  sublevolico  46021  ismbl3  46023  ovolsplit  46025  volioore  46027  voliooico  46029  voliccico  46036  stoweidlem14  46051  stoweidlem26  46063  stoweidlem28  46065  stoweidlem55  46092  stoweid  46100  stirlinglem5  46115  stirlinglem12  46122  dirkerper  46133  dirkertrigeqlem3  46137  dirkertrigeq  46138  dirkercncflem1  46140  dirkercncflem2  46141  dirkercncf  46144  fourierdlem10  46154  fourierdlem12  46156  fourierdlem24  46168  fourierdlem30  46174  fourierdlem31  46175  fourierdlem32  46176  fourierdlem33  46177  fourierdlem34  46178  fourierdlem35  46179  fourierdlem37  46181  fourierdlem40  46184  fourierdlem41  46185  fourierdlem42  46186  fourierdlem43  46187  fourierdlem44  46188  fourierdlem46  46189  fourierdlem48  46191  fourierdlem49  46192  fourierdlem51  46194  fourierdlem54  46197  fourierdlem62  46205  fourierdlem64  46207  fourierdlem65  46208  fourierdlem70  46213  fourierdlem71  46214  fourierdlem73  46216  fourierdlem74  46217  fourierdlem75  46218  fourierdlem78  46221  fourierdlem79  46222  fourierdlem80  46223  fourierdlem81  46224  fourierdlem82  46225  fourierdlem92  46235  fourierdlem93  46236  fourierdlem97  46240  fourierdlem101  46244  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem109  46252  fourierdlem114  46257  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  elaa2lem  46270  etransclem15  46286  etransclem19  46290  etransclem20  46291  etransclem22  46293  etransclem23  46294  etransclem24  46295  etransclem25  46296  etransclem27  46298  etransclem28  46299  etransclem35  46306  etransclem38  46309  qndenserrnbl  46332  ioorrnopn  46342  ioorrnopnxrlem  46343  ioorrnopnxr  46344  prsal  46355  salexct  46371  issalnnd  46382  sge0sn  46416  sge0tsms  46417  sge0cl  46418  sge0f1o  46419  sge0sup  46428  sge0less  46429  sge0pr  46431  sge0prle  46438  sge0le  46444  sge0split  46446  sge0splitmpt  46448  sge0iunmptlemfi  46450  sge0iunmpt  46455  sge0isum  46464  sge0xaddlem1  46470  sge0xadd  46472  sge0gtfsumgt  46480  nnfoctbdjlem  46492  iundjiun  46497  meadjun  46499  ismeannd  46504  voliunsge0lem  46509  meaiuninc3v  46521  caragenfiiuncl  46552  omeiunltfirp  46556  carageniuncl  46560  caragenunicl  46561  isomenndlem  46567  isomennd  46568  hoicvr  46585  ovnssle  46598  ovn0  46603  ovnsubadd  46609  hsphoidmvle2  46622  hoidmvval0b  46627  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmv1le  46631  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem5  46636  hoidmvle  46637  ovnhoilem1  46638  ovnhoi  46640  ovnlecvr2  46647  hspdifhsp  46653  hoidifhspdmvle  46657  hoiqssbl  46662  hspmbllem1  46663  hspmbllem2  46664  hspmbl  46666  hoimbl  46668  volico2  46678  ovolval2lem  46680  ovnsubadd2lem  46682  ovolval4lem1  46686  ovolval4lem2  46687  ovolval5lem1  46689  vonhoire  46709  iunhoiioo  46713  vonioo  46719  vonicc  46722  vonsn  46728  pimrecltpos  46745  incsmflem  46778  smfpimltxr  46784  smfconst  46786  decsmflem  46803  smfpimgtxr  46817  smfrec  46826  smfpimne2  46877  sharhght  46902  rrx2linest  48773  mofsn2  48875  ipolub00  49023  resccat  49105  initopropdlemlem  49270  prcof1  49419