Theorem pm2.61dan 813

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  814  pm2.61dda  815  nfsb4t  2504  sbal2  2534  pm2.61danel  3060  ifeq1da  4557  ifeq2da  4558  ifeq12da  4559  ifclda  4561  ifeqda  4562  ifbothda  4564  2if2  4581  somin1  6153  xpcan  6196  fvmpti  7015  fvmptss  7028  funressn  7179  ovima0  7612  ordsuci  7828  suppssov1  8222  suppssov2  8223  oeoa  8635  oeoe  8637  omabs  8689  eceqoveq  8862  domdifsn  9094  pw2f1olem  9116  mapdom1  9182  imafiOLD  9354  marypha1lem  9473  supval2  9495  infdifsn  9697  ttrcltr  9756  ttrclselem1  9765  carden2b  10007  fidomtri  10033  dfac12lem2  10185  infunsdom1  10252  infunsdom  10253  itunisuc  10459  gchdomtri  10669  fiminre2  12216  xrmax2  13218  xrmin1  13219  ifle  13239  xnn0lem1lt  13286  xmulneg1  13311  xrsupsslem  13349  xrinfmsslem  13350  fzneuz  13648  seqf1olem1  14082  bccmpl  14348  bcval5  14357  bcpasc  14360  bccl  14361  hasheni  14387  hashfn  14414  hashdom  14418  hashdomi  14419  hashge1  14428  hashbc  14492  pfxval0  14714  sumz  15758  sumss  15760  fsumsplitsn  15780  sumsplit  15804  prod1  15980  prodss  15983  fprodsplitsn  16025  fprodle  16032  bitsmod  16473  sadadd2lem2  16487  sadcaddlem  16494  gcddvds  16540  gcdcl  16543  gcdneg  16559  dvdslcm  16635  lcmcl  16638  lcmneg  16640  lcmgcd  16644  lcmfcl  16665  dvdslcmf  16668  pcgcd  16916  pcmpt  16930  pcmpt2  16931  pcprod  16933  fldivp1  16935  prmreclem4  16957  vdwlem6  17024  ramub1lem1  17064  cidpropd  17753  rescabs  17877  rescabsOLD  17878  lubval  18401  glbval  18414  joinval  18422  meetval  18436  acsexdimd  18604  gsumpropd2lem  18692  gsumval2  18699  mulgfval  19087  f1otrspeq  19465  pmtrfinv  19479  psgnunilem1  19511  gsumval3  19925  ablfac1c  20091  ablfac1eu  20093  mgpress  20147  frlmsslsp  21816  psrbas  21953  resspsrbas  21994  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  opsrle  22065  opsrbaslem  22067  opsrbaslemOLD  22068  psrbaspropd  22236  mplbaspropd  22238  mdetdiag  22605  mdetunilem7  22624  mdetunilem9  22626  maducoeval2  22646  madurid  22650  opnnei  23128  restbas  23166  hauspwdom  23509  ptcmplem5  24064  xrsmopn  24834  xrhmeo  24977  lebnum  24996  pcoass  25057  pcorevlem  25059  icombl  25599  ioombl  25600  mbfconstlem  25662  mbfima  25665  i1fd  25716  mbfi1fseqlem5  25754  itg2const2  25776  itg2seq  25777  itg2uba  25778  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  iblss2  25841  itgss  25847  bddmulibl  25874  coemullem  26289  aaliou2b  26383  isppw2  27158  mule1  27191  ppip1le  27204  dchrelbas3  27282  dchrpt  27311  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgslem4  27344  lgsneg  27365  lgsmod  27367  lgsdilem  27368  lgsdir  27376  lgsdi  27378  lgsne0  27379  lgsquad3  27431  dchrvmasum2if  27541  maxs2  27811  mins1  27812  midexlem  28700  colperpex  28741  outpasch  28763  hlpasch  28764  lnopp2hpgb  28771  lmieu  28792  inaghl  28853  cgrg3col4  28861  pthdlem1  29786  nmcfnlbi  32071  elpreq  32548  disjdifprg  32588  disjun0  32608  f1ocnt  32804  xrge0npcan  33025  psgnfzto1stlem  33120  cyc3genpmlem  33171  cyc3conja  33177  archiabl  33205  erlval  33262  orngsqr  33334  1arithufdlem3  33574  1arithufd  33576  resssra  33638  lbslelsp  33648  1smat1  33803  esumcst  34064  esumrnmpt2  34069  hasheuni  34086  esumcvg  34087  ddemeas  34237  omssubadd  34302  eulerpartlemgc  34364  eulerpartlemb  34370  plymulx  34563  signswmnd  34572  pthhashvtx  35133  erdsze2lem1  35208  mrsubvrs  35527  unblimceq0lem  36507  unbdqndv2lem2  36511  knoppndvlem10  36522  wl-spae  37522  wl-cbvalnaed  37533  wl-nfeqfb  37537  unccur  37610  poimirlem15  37642  poimirlem22  37649  itg2addnclem  37678  itg2addnclem2  37679  iblmulc2nc  37692  ftc1anclem5  37704  ftc1anc  37708  dvasin  37711  areacirclem5  37719  exmid2  38106  3dim1  39469  3dim2  39470  3dim3  39471  3atlem3  39487  3atlem7  39491  lvolnle3at  39584  2lplnja  39621  paddasslem18  39839  lhpexle3lem  40013  4atex  40078  cdlemd5  40204  cdleme16  40287  cdleme20  40326  cdleme21j  40338  cdleme21  40339  cdleme32snaw  40437  cdleme32fvcl  40442  cdleme32le  40449  cdlemeg46gf  40535  cdleme48gfv  40539  cdleme50trn12  40554  cdlemg6  40625  cdlemg7N  40628  cdlemg38  40717  cdlemg46  40737  dibvalrel  41165  dihlss  41252  dihglblem5aN  41294  dihmeetbN  41305  dihmeetALTN  41329  dihatlat  41336  dihatexv  41340  dvh3dim2  41450  dvh3dim3N  41451  lclkrlem2h  41516  mapdh8d  41785  mapdh8g  41787  hdmap11lem2  41844  lcmineqlem23  42052  aks4d1p3  42079  aks4d1p5  42081  aks4d1p7d1  42083  posbezout  42101  aks6d1c2p2  42120  aks6d1c4  42125  aks6d1c5lem1  42137  aks6d1c6lem3  42173  aks6d1c6lem4  42174  bcled  42179  bcle2d  42180  aks6d1c7  42185  grpods  42195  unitscyglem2  42197  unitscyglem4  42199  aks5lem8  42202  metakunt23  42228  metakunt24  42229  metakunt29  42234  metakunt30  42235  metakunt31  42236  dffltz  42644  ttac  43048  pw2f1ocnv  43049  aomclem5  43070  isnumbasgrplem3  43117  iocmbl  43225  oe0suclim  43290  tfsconcatfv  43354  safesnsupfidom1o  43430  safesnsupfilb  43431  r1rankcld  44250  grur1cld  44251  grucollcld  44279  mnuprd  44295  radcnvrat  44333  bccbc  44364  binomcxp  44376  fnchoice  45034  fiiuncl  45070  eliin2f  45109  founiiun0  45195  axccdom  45227  axccd2  45235  fzisoeu  45312  fperiodmul  45316  upbdrech2  45320  fzdifsuc2  45322  uzfissfz  45337  supxrgere  45344  supxrgelem  45348  supxrge  45349  suplesup  45350  infrpge  45362  xrlexaddrp  45363  xralrple2  45365  infxr  45378  infleinflem1  45381  infleinflem2  45382  infleinf  45383  xralrple3  45385  xrralrecnnge  45401  uzublem  45441  supxrmnf2  45444  infxrpnf  45457  infxrpnf2  45474  supminfxr  45475  supminfxr2  45480  pimxrneun  45499  rexanuz2nf  45503  ioondisj2  45506  iccdifprioo  45529  fmul01lt1lem1  45599  fmul01lt1lem2  45600  limciccioolb  45636  lptioo2  45646  lptioo1  45647  limcicciooub  45652  lptre2pt  45655  limcresiooub  45657  limcresioolb  45658  limcleqr  45659  climfveq  45684  climfveqf  45695  limsupubuzlem  45727  limsupubuz  45728  limsupmnfuzlem  45741  limsupre3uzlem  45750  climxrre  45765  limsup10exlem  45787  cnrefiisplem  45844  climxlim2lem  45860  dfxlim2v  45862  xlimliminflimsup  45877  coskpi2  45881  cosknegpi  45884  icccncfext  45902  cncfiooicclem1  45908  cncfiooicc  45909  cncfiooiccre  45910  dvbdfbdioolem2  45944  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnprodlem1  45961  dvnprodlem3  45963  volioc  45987  itgioocnicc  45992  iblcncfioo  45993  volico  45998  sublevolico  45999  ismbl3  46001  ovolsplit  46003  volioore  46005  voliooico  46007  voliccico  46014  stoweidlem14  46029  stoweidlem26  46041  stoweidlem28  46043  stoweidlem55  46070  stoweid  46078  stirlinglem5  46093  stirlinglem12  46100  dirkerper  46111  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncf  46122  fourierdlem10  46132  fourierdlem12  46134  fourierdlem24  46146  fourierdlem30  46152  fourierdlem31  46153  fourierdlem32  46154  fourierdlem33  46155  fourierdlem34  46156  fourierdlem35  46157  fourierdlem37  46159  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem43  46165  fourierdlem44  46166  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem54  46175  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem79  46200  fourierdlem80  46201  fourierdlem81  46202  fourierdlem82  46203  fourierdlem92  46213  fourierdlem93  46214  fourierdlem97  46218  fourierdlem101  46222  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem109  46230  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  elaa2lem  46248  etransclem15  46264  etransclem19  46268  etransclem20  46269  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem27  46276  etransclem28  46277  etransclem35  46284  etransclem38  46287  qndenserrnbl  46310  ioorrnopn  46320  ioorrnopnxrlem  46321  ioorrnopnxr  46322  prsal  46333  salexct  46349  issalnnd  46360  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0sup  46406  sge0less  46407  sge0pr  46409  sge0prle  46416  sge0le  46422  sge0split  46424  sge0splitmpt  46426  sge0iunmptlemfi  46428  sge0iunmpt  46433  sge0isum  46442  sge0xaddlem1  46448  sge0xadd  46450  sge0gtfsumgt  46458  nnfoctbdjlem  46470  iundjiun  46475  meadjun  46477  ismeannd  46482  voliunsge0lem  46487  meaiuninc3v  46499  caragenfiiuncl  46530  omeiunltfirp  46534  carageniuncl  46538  caragenunicl  46539  isomenndlem  46545  isomennd  46546  hoicvr  46563  ovnssle  46576  ovn0  46581  ovnsubadd  46587  hsphoidmvle2  46600  hoidmvval0b  46605  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem5  46614  hoidmvle  46615  ovnhoilem1  46616  ovnhoi  46618  ovnlecvr2  46625  hspdifhsp  46631  hoidifhspdmvle  46635  hoiqssbl  46640  hspmbllem1  46641  hspmbllem2  46642  hspmbl  46644  hoimbl  46646  volico2  46656  ovolval2lem  46658  ovnsubadd2lem  46660  ovolval4lem1  46664  ovolval4lem2  46665  ovolval5lem1  46667  vonhoire  46687  iunhoiioo  46691  vonioo  46697  vonicc  46700  vonsn  46706  pimrecltpos  46723  incsmflem  46756  smfpimltxr  46762  smfconst  46764  decsmflem  46781  smfpimgtxr  46795  smfrec  46804  smfpimne2  46855  sharhght  46880  rrx2linest  48663  mofsn2  48754  ipolub00  48882