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  2497  sbal2  2527  pm2.61danel  3043  ifeq1da  4504  ifeq2da  4505  ifeq12da  4506  ifclda  4508  ifeqda  4509  ifbothda  4511  2if2  4528  somin1  6076  xpcan  6119  fvmpti  6922  fvmptss  6935  funressn  7086  ovima0  7519  ordsuci  7735  suppssov1  8121  suppssov2  8122  oeoa  8506  oeoe  8508  omabs  8560  eceqoveq  8740  domdifsn  8967  pw2f1olem  8988  mapdom1  9049  imafiOLD  9194  marypha1lem  9311  supval2  9333  infdifsn  9541  ttrcltr  9600  ttrclselem1  9609  carden2b  9851  fidomtri  9877  dfac12lem2  10027  infunsdom1  10094  infunsdom  10095  itunisuc  10301  gchdomtri  10511  fiminre2  12061  xrmax2  13066  xrmin1  13067  ifle  13087  xnn0lem1lt  13134  xmulneg1  13159  xrsupsslem  13197  xrinfmsslem  13198  fzneuz  13499  seqf1olem1  13936  bccmpl  14204  bcval5  14213  bcpasc  14216  bccl  14217  hasheni  14243  hashfn  14270  hashdom  14274  hashdomi  14275  hashge1  14284  hashbc  14348  pfxval0  14571  sumz  15616  sumss  15618  fsumsplitsn  15638  sumsplit  15662  prod1  15838  prodss  15841  fprodsplitsn  15883  fprodle  15890  bitsmod  16334  sadadd2lem2  16348  sadcaddlem  16355  gcddvds  16401  gcdcl  16404  gcdneg  16420  dvdslcm  16496  lcmcl  16499  lcmneg  16501  lcmgcd  16505  lcmfcl  16526  dvdslcmf  16529  pcgcd  16777  pcmpt  16791  pcmpt2  16792  pcprod  16794  fldivp1  16796  prmreclem4  16818  vdwlem6  16885  ramub1lem1  16925  cidpropd  17603  rescabs  17727  lubval  18247  glbval  18260  joinval  18268  meetval  18282  acsexdimd  18452  gsumpropd2lem  18540  gsumval2  18547  mulgfval  18935  f1otrspeq  19313  pmtrfinv  19327  psgnunilem1  19359  gsumval3  19773  ablfac1c  19939  ablfac1eu  19941  mgpress  20022  orngsqr  20735  frlmsslsp  21687  psrbas  21824  resspsrbas  21865  mplmonmul  21925  mplcoe1  21926  mplcoe5  21929  opsrle  21936  opsrbaslem  21938  psrbaspropd  22101  mplbaspropd  22103  mdetdiag  22468  mdetunilem7  22487  mdetunilem9  22489  maducoeval2  22509  madurid  22513  opnnei  22989  restbas  23027  hauspwdom  23370  ptcmplem5  23925  xrsmopn  24682  xrhmeo  24825  lebnum  24844  pcoass  24905  pcorevlem  24907  icombl  25446  ioombl  25447  mbfconstlem  25509  mbfima  25512  i1fd  25563  mbfi1fseqlem5  25601  itg2const2  25623  itg2seq  25624  itg2uba  25625  itg2splitlem  25630  itg2split  25631  itg2monolem1  25632  itg2gt0  25642  itg2cnlem1  25643  itg2cnlem2  25644  iblss  25687  iblss2  25688  itgss  25694  bddmulibl  25721  coemullem  26136  aaliou2b  26230  isppw2  27006  mule1  27039  ppip1le  27052  dchrelbas3  27130  dchrpt  27159  bposlem3  27178  bposlem5  27180  bposlem6  27181  lgslem4  27192  lgsneg  27213  lgsmod  27215  lgsdilem  27216  lgsdir  27224  lgsdi  27226  lgsne0  27227  lgsquad3  27279  dchrvmasum2if  27389  maxs2  27659  mins1  27660  midexlem  28624  colperpex  28665  outpasch  28687  hlpasch  28688  lnopp2hpgb  28695  lmieu  28716  inaghl  28777  cgrg3col4  28785  pthdlem1  29698  nmcfnlbi  31983  elpreq  32460  prssad  32461  prssbd  32462  disjdifprg  32507  disjun0  32527  argcj  32684  f1ocnt  32737  xrge0npcan  32969  psgnfzto1stlem  33037  cyc3genpmlem  33088  cyc3conja  33094  archiabl  33135  erlval  33193  1arithufdlem3  33479  1arithufd  33481  resssra  33567  lbslelsp  33578  constrrecl  33750  constrinvcl  33754  constrsqrtcl  33760  1smat1  33785  esumcst  34044  esumrnmpt2  34049  hasheuni  34066  esumcvg  34067  ddemeas  34217  omssubadd  34281  eulerpartlemgc  34343  eulerpartlemb  34349  plymulx  34529  signswmnd  34538  fineqvnttrclselem1  35087  pthhashvtx  35118  erdsze2lem1  35193  mrsubvrs  35512  unblimceq0lem  36497  unbdqndv2lem2  36501  knoppndvlem10  36512  wl-spae  37512  wl-cbvalnaed  37523  wl-nfeqfb  37527  unccur  37600  poimirlem15  37632  poimirlem22  37639  itg2addnclem  37668  itg2addnclem2  37669  iblmulc2nc  37682  ftc1anclem5  37694  ftc1anc  37698  dvasin  37701  areacirclem5  37709  exmid2  38096  3dim1  39463  3dim2  39464  3dim3  39465  3atlem3  39481  3atlem7  39485  lvolnle3at  39578  2lplnja  39615  paddasslem18  39833  lhpexle3lem  40007  4atex  40072  cdlemd5  40198  cdleme16  40281  cdleme20  40320  cdleme21j  40332  cdleme21  40333  cdleme32snaw  40431  cdleme32fvcl  40436  cdleme32le  40443  cdlemeg46gf  40529  cdleme48gfv  40533  cdleme50trn12  40548  cdlemg6  40619  cdlemg7N  40622  cdlemg38  40711  cdlemg46  40731  dibvalrel  41159  dihlss  41246  dihglblem5aN  41288  dihmeetbN  41299  dihmeetALTN  41323  dihatlat  41330  dihatexv  41334  dvh3dim2  41444  dvh3dim3N  41445  lclkrlem2h  41510  mapdh8d  41779  mapdh8g  41781  hdmap11lem2  41838  lcmineqlem23  42041  aks4d1p3  42068  aks4d1p5  42070  aks4d1p7d1  42072  posbezout  42090  aks6d1c2p2  42109  aks6d1c4  42114  aks6d1c5lem1  42126  aks6d1c6lem3  42162  aks6d1c6lem4  42163  bcled  42168  bcle2d  42169  aks6d1c7  42174  grpods  42184  unitscyglem2  42186  unitscyglem4  42188  aks5lem8  42191  dffltz  42624  ttac  43026  pw2f1ocnv  43027  aomclem5  43048  isnumbasgrplem3  43095  iocmbl  43203  oe0suclim  43267  tfsconcatfv  43331  safesnsupfidom1o  43407  safesnsupfilb  43408  r1rankcld  44221  grur1cld  44222  grucollcld  44250  mnuprd  44266  radcnvrat  44304  bccbc  44335  binomcxp  44347  fnchoice  45023  fiiuncl  45059  eliin2f  45098  founiiun0  45184  axccdom  45216  axccd2  45224  fzisoeu  45298  fperiodmul  45302  upbdrech2  45306  fzdifsuc2  45308  uzfissfz  45322  supxrgere  45329  supxrgelem  45333  supxrge  45334  suplesup  45335  infrpge  45347  xrlexaddrp  45348  xralrple2  45350  infxr  45362  infleinflem1  45365  infleinflem2  45366  infleinf  45367  xralrple3  45369  xrralrecnnge  45385  uzublem  45425  supxrmnf2  45428  infxrpnf  45441  infxrpnf2  45458  supminfxr  45459  supminfxr2  45464  pimxrneun  45483  rexanuz2nf  45487  ioondisj2  45490  iccdifprioo  45513  fmul01lt1lem1  45581  fmul01lt1lem2  45582  limciccioolb  45618  lptioo2  45628  lptioo1  45629  limcicciooub  45632  lptre2pt  45635  limcresiooub  45637  limcresioolb  45638  limcleqr  45639  climfveq  45664  climfveqf  45675  limsupubuzlem  45707  limsupubuz  45708  limsupmnfuzlem  45721  limsupre3uzlem  45730  climxrre  45745  limsup10exlem  45767  cnrefiisplem  45824  climxlim2lem  45840  dfxlim2v  45842  xlimliminflimsup  45857  coskpi2  45861  cosknegpi  45864  icccncfext  45882  cncfiooicclem1  45888  cncfiooicc  45889  cncfiooiccre  45890  dvbdfbdioolem2  45924  ioodvbdlimc1lem1  45926  ioodvbdlimc1lem2  45927  ioodvbdlimc2lem  45929  dvnxpaek  45937  dvnprodlem1  45941  dvnprodlem3  45943  volioc  45967  itgioocnicc  45972  iblcncfioo  45973  volico  45978  sublevolico  45979  ismbl3  45981  ovolsplit  45983  volioore  45985  voliooico  45987  voliccico  45994  stoweidlem14  46009  stoweidlem26  46021  stoweidlem28  46023  stoweidlem55  46050  stoweid  46058  stirlinglem5  46073  stirlinglem12  46080  dirkerper  46091  dirkertrigeqlem3  46095  dirkertrigeq  46096  dirkercncflem1  46098  dirkercncflem2  46099  dirkercncf  46102  fourierdlem10  46112  fourierdlem12  46114  fourierdlem24  46126  fourierdlem30  46132  fourierdlem31  46133  fourierdlem32  46134  fourierdlem33  46135  fourierdlem34  46136  fourierdlem35  46137  fourierdlem37  46139  fourierdlem40  46142  fourierdlem41  46143  fourierdlem42  46144  fourierdlem43  46145  fourierdlem44  46146  fourierdlem46  46147  fourierdlem48  46149  fourierdlem49  46150  fourierdlem51  46152  fourierdlem54  46155  fourierdlem62  46163  fourierdlem64  46165  fourierdlem65  46166  fourierdlem70  46171  fourierdlem71  46172  fourierdlem73  46174  fourierdlem74  46175  fourierdlem75  46176  fourierdlem78  46179  fourierdlem79  46180  fourierdlem80  46181  fourierdlem81  46182  fourierdlem82  46183  fourierdlem92  46193  fourierdlem93  46194  fourierdlem97  46198  fourierdlem101  46202  fourierdlem102  46203  fourierdlem103  46204  fourierdlem104  46205  fourierdlem109  46210  fourierdlem114  46215  sqwvfoura  46223  sqwvfourb  46224  fourierswlem  46225  fouriersw  46226  elaa2lem  46228  etransclem15  46244  etransclem19  46248  etransclem20  46249  etransclem22  46251  etransclem23  46252  etransclem24  46253  etransclem25  46254  etransclem27  46256  etransclem28  46257  etransclem35  46264  etransclem38  46267  qndenserrnbl  46290  ioorrnopn  46300  ioorrnopnxrlem  46301  ioorrnopnxr  46302  prsal  46313  salexct  46329  issalnnd  46340  sge0sn  46374  sge0tsms  46375  sge0cl  46376  sge0f1o  46377  sge0sup  46386  sge0less  46387  sge0pr  46389  sge0prle  46396  sge0le  46402  sge0split  46404  sge0splitmpt  46406  sge0iunmptlemfi  46408  sge0iunmpt  46413  sge0isum  46422  sge0xaddlem1  46428  sge0xadd  46430  sge0gtfsumgt  46438  nnfoctbdjlem  46450  iundjiun  46455  meadjun  46457  ismeannd  46462  voliunsge0lem  46467  meaiuninc3v  46479  caragenfiiuncl  46510  omeiunltfirp  46514  carageniuncl  46518  caragenunicl  46519  isomenndlem  46525  isomennd  46526  hoicvr  46543  ovnssle  46556  ovn0  46561  ovnsubadd  46567  hsphoidmvle2  46580  hoidmvval0b  46585  hoidmv1lelem1  46586  hoidmv1lelem2  46587  hoidmv1le  46589  hoidmvlelem2  46591  hoidmvlelem3  46592  hoidmvlelem5  46594  hoidmvle  46595  ovnhoilem1  46596  ovnhoi  46598  ovnlecvr2  46605  hspdifhsp  46611  hoidifhspdmvle  46615  hoiqssbl  46620  hspmbllem1  46621  hspmbllem2  46622  hspmbl  46624  hoimbl  46626  volico2  46636  ovolval2lem  46638  ovnsubadd2lem  46640  ovolval4lem1  46644  ovolval4lem2  46645  ovolval5lem1  46647  vonhoire  46667  iunhoiioo  46671  vonioo  46677  vonicc  46680  vonsn  46686  pimrecltpos  46703  incsmflem  46736  smfpimltxr  46742  smfconst  46744  decsmflem  46761  smfpimgtxr  46775  smfrec  46784  smfpimne2  46835  sharhght  46860  rrx2linest  48741  mofsn2  48843  ipolub00  48991  resccat  49073  initopropdlemlem  49238  prcof1  49387