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  2507  sbal2  2537  pm2.61danel  3066  ifeq1da  4579  ifeq2da  4580  ifeq12da  4581  ifclda  4583  ifeqda  4584  ifbothda  4586  2if2  4603  somin1  6165  xpcan  6207  fvmpti  7028  fvmptss  7041  funressn  7193  ovima0  7629  ordsuci  7844  suppssov1  8238  suppssov2  8239  oeoa  8653  oeoe  8655  omabs  8707  eceqoveq  8880  domdifsn  9120  pw2f1olem  9142  mapdom1  9208  imafiOLD  9382  marypha1lem  9502  supval2  9524  infdifsn  9726  ttrcltr  9785  ttrclselem1  9794  carden2b  10036  fidomtri  10062  dfac12lem2  10214  infunsdom1  10281  infunsdom  10282  itunisuc  10488  gchdomtri  10698  fiminre2  12243  xrmax2  13238  xrmin1  13239  ifle  13259  xnn0lem1lt  13306  xmulneg1  13331  xrsupsslem  13369  xrinfmsslem  13370  fzneuz  13665  seqf1olem1  14092  bccmpl  14358  bcval5  14367  bcpasc  14370  bccl  14371  hasheni  14397  hashfn  14424  hashdom  14428  hashdomi  14429  hashge1  14438  hashbc  14502  pfxval0  14724  sumz  15770  sumss  15772  fsumsplitsn  15792  sumsplit  15816  prod1  15992  prodss  15995  fprodsplitsn  16037  fprodle  16044  bitsmod  16482  sadadd2lem2  16496  sadcaddlem  16503  gcddvds  16549  gcdcl  16552  gcdneg  16568  dvdslcm  16645  lcmcl  16648  lcmneg  16650  lcmgcd  16654  lcmfcl  16675  dvdslcmf  16678  pcgcd  16925  pcmpt  16939  pcmpt2  16940  pcprod  16942  fldivp1  16944  prmreclem4  16966  vdwlem6  17033  ramub1lem1  17073  cidpropd  17768  rescabs  17896  rescabsOLD  17897  lubval  18426  glbval  18439  joinval  18447  meetval  18461  acsexdimd  18629  gsumpropd2lem  18717  gsumval2  18724  mulgfval  19109  f1otrspeq  19489  pmtrfinv  19503  psgnunilem1  19535  gsumval3  19949  ablfac1c  20115  ablfac1eu  20117  mgpress  20176  mgpressOLD  20177  frlmsslsp  21839  psrbas  21976  resspsrbas  22017  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  opsrle  22088  opsrbaslem  22090  opsrbaslemOLD  22091  psrbaspropd  22257  mplbaspropd  22259  mdetdiag  22626  mdetunilem7  22645  mdetunilem9  22647  maducoeval2  22667  madurid  22671  opnnei  23149  restbas  23187  hauspwdom  23530  ptcmplem5  24085  xrsmopn  24853  xrhmeo  24996  lebnum  25015  pcoass  25076  pcorevlem  25078  icombl  25618  ioombl  25619  mbfconstlem  25681  mbfima  25684  i1fd  25735  mbfi1fseqlem5  25774  itg2const2  25796  itg2seq  25797  itg2uba  25798  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  iblss  25860  iblss2  25861  itgss  25867  bddmulibl  25894  coemullem  26309  aaliou2b  26401  isppw2  27176  mule1  27209  ppip1le  27222  dchrelbas3  27300  dchrpt  27329  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgslem4  27362  lgsneg  27383  lgsmod  27385  lgsdilem  27386  lgsdir  27394  lgsdi  27396  lgsne0  27397  lgsquad3  27449  dchrvmasum2if  27559  maxs2  27829  mins1  27830  midexlem  28718  colperpex  28759  outpasch  28781  hlpasch  28782  lnopp2hpgb  28789  lmieu  28810  inaghl  28871  cgrg3col4  28879  pthdlem1  29802  nmcfnlbi  32084  elpreq  32558  disjdifprg  32597  disjun0  32617  f1ocnt  32807  xrge0npcan  33006  psgnfzto1stlem  33093  cyc3genpmlem  33144  cyc3conja  33150  archiabl  33178  erlval  33230  orngsqr  33299  1arithufdlem3  33539  1arithufd  33541  resssra  33602  1smat1  33750  esumcst  34027  esumrnmpt2  34032  hasheuni  34049  esumcvg  34050  ddemeas  34200  omssubadd  34265  eulerpartlemgc  34327  eulerpartlemb  34333  plymulx  34525  signswmnd  34534  pthhashvtx  35095  erdsze2lem1  35171  mrsubvrs  35490  unblimceq0lem  36472  unbdqndv2lem2  36476  knoppndvlem10  36487  wl-spae  37475  wl-cbvalnaed  37486  wl-nfeqfb  37490  unccur  37563  poimirlem15  37595  poimirlem22  37602  itg2addnclem  37631  itg2addnclem2  37632  iblmulc2nc  37645  ftc1anclem5  37657  ftc1anc  37661  dvasin  37664  areacirclem5  37672  exmid2  38059  3dim1  39424  3dim2  39425  3dim3  39426  3atlem3  39442  3atlem7  39446  lvolnle3at  39539  2lplnja  39576  paddasslem18  39794  lhpexle3lem  39968  4atex  40033  cdlemd5  40159  cdleme16  40242  cdleme20  40281  cdleme21j  40293  cdleme21  40294  cdleme32snaw  40392  cdleme32fvcl  40397  cdleme32le  40404  cdlemeg46gf  40490  cdleme48gfv  40494  cdleme50trn12  40509  cdlemg6  40580  cdlemg7N  40583  cdlemg38  40672  cdlemg46  40692  dibvalrel  41120  dihlss  41207  dihglblem5aN  41249  dihmeetbN  41260  dihmeetALTN  41284  dihatlat  41291  dihatexv  41295  dvh3dim2  41405  dvh3dim3N  41406  lclkrlem2h  41471  mapdh8d  41740  mapdh8g  41742  hdmap11lem2  41799  lcmineqlem23  42008  aks4d1p3  42035  aks4d1p5  42037  aks4d1p7d1  42039  posbezout  42057  aks6d1c2p2  42076  aks6d1c4  42081  aks6d1c5lem1  42093  aks6d1c6lem3  42129  aks6d1c6lem4  42130  bcled  42135  bcle2d  42136  aks6d1c7  42141  grpods  42151  unitscyglem2  42153  unitscyglem4  42155  aks5lem8  42158  metakunt23  42184  metakunt24  42185  metakunt29  42190  metakunt30  42191  metakunt31  42192  dffltz  42589  ttac  42993  pw2f1ocnv  42994  aomclem5  43015  isnumbasgrplem3  43062  iocmbl  43174  oe0suclim  43239  tfsconcatfv  43303  safesnsupfidom1o  43379  safesnsupfilb  43380  r1rankcld  44200  grur1cld  44201  grucollcld  44229  mnuprd  44245  radcnvrat  44283  bccbc  44314  binomcxp  44326  fnchoice  44929  fiiuncl  44967  eliin2f  45006  founiiun0  45097  axccdom  45129  axccd2  45137  fzisoeu  45215  fperiodmul  45219  upbdrech2  45223  fzdifsuc2  45225  uzfissfz  45241  supxrgere  45248  supxrgelem  45252  supxrge  45253  suplesup  45254  infrpge  45266  xrlexaddrp  45267  xralrple2  45269  infxr  45282  infleinflem1  45285  infleinflem2  45286  infleinf  45287  xralrple3  45289  xrralrecnnge  45305  uzublem  45345  supxrmnf2  45348  infxrpnf  45361  infxrpnf2  45378  supminfxr  45379  supminfxr2  45384  pimxrneun  45404  rexanuz2nf  45408  ioondisj2  45411  iccdifprioo  45434  fmul01lt1lem1  45505  fmul01lt1lem2  45506  limciccioolb  45542  lptioo2  45552  lptioo1  45553  limcicciooub  45558  lptre2pt  45561  limcresiooub  45563  limcresioolb  45564  limcleqr  45565  climfveq  45590  climfveqf  45601  limsupubuzlem  45633  limsupubuz  45634  limsupmnfuzlem  45647  limsupre3uzlem  45656  climxrre  45671  limsup10exlem  45693  cnrefiisplem  45750  climxlim2lem  45766  dfxlim2v  45768  xlimliminflimsup  45783  coskpi2  45787  cosknegpi  45790  icccncfext  45808  cncfiooicclem1  45814  cncfiooicc  45815  cncfiooiccre  45816  dvbdfbdioolem2  45850  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnprodlem1  45867  dvnprodlem3  45869  volioc  45893  itgioocnicc  45898  iblcncfioo  45899  volico  45904  sublevolico  45905  ismbl3  45907  ovolsplit  45909  volioore  45911  voliooico  45913  voliccico  45920  stoweidlem14  45935  stoweidlem26  45947  stoweidlem28  45949  stoweidlem55  45976  stoweid  45984  stirlinglem5  45999  stirlinglem12  46006  dirkerper  46017  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncf  46028  fourierdlem10  46038  fourierdlem12  46040  fourierdlem24  46052  fourierdlem30  46058  fourierdlem31  46059  fourierdlem32  46060  fourierdlem33  46061  fourierdlem34  46062  fourierdlem35  46063  fourierdlem37  46065  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem43  46071  fourierdlem44  46072  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem54  46081  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem79  46106  fourierdlem80  46107  fourierdlem81  46108  fourierdlem82  46109  fourierdlem92  46119  fourierdlem93  46120  fourierdlem97  46124  fourierdlem101  46128  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem109  46136  fourierdlem114  46141  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem15  46170  etransclem19  46174  etransclem20  46175  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem27  46182  etransclem28  46183  etransclem35  46190  etransclem38  46193  qndenserrnbl  46216  ioorrnopn  46226  ioorrnopnxrlem  46227  ioorrnopnxr  46228  prsal  46239  salexct  46255  issalnnd  46266  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0sup  46312  sge0less  46313  sge0pr  46315  sge0prle  46322  sge0le  46328  sge0split  46330  sge0splitmpt  46332  sge0iunmptlemfi  46334  sge0iunmpt  46339  sge0isum  46348  sge0xaddlem1  46354  sge0xadd  46356  sge0gtfsumgt  46364  nnfoctbdjlem  46376  iundjiun  46381  meadjun  46383  ismeannd  46388  voliunsge0lem  46393  meaiuninc3v  46405  caragenfiiuncl  46436  omeiunltfirp  46440  carageniuncl  46444  caragenunicl  46445  isomenndlem  46451  isomennd  46452  hoicvr  46469  ovnssle  46482  ovn0  46487  ovnsubadd  46493  hsphoidmvle2  46506  hoidmvval0b  46511  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem5  46520  hoidmvle  46521  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  hspdifhsp  46537  hoidifhspdmvle  46541  hoiqssbl  46546  hspmbllem1  46547  hspmbllem2  46548  hspmbl  46550  hoimbl  46552  volico2  46562  ovolval2lem  46564  ovnsubadd2lem  46566  ovolval4lem1  46570  ovolval4lem2  46571  ovolval5lem1  46573  vonhoire  46593  iunhoiioo  46597  vonioo  46603  vonicc  46606  vonsn  46612  pimrecltpos  46629  incsmflem  46662  smfpimltxr  46668  smfconst  46670  decsmflem  46687  smfpimgtxr  46701  smfrec  46710  smfpimne2  46761  sharhght  46786  rrx2linest  48476  mofsn2  48558  ipolub00  48665