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  3051  ifeq1da  4499  ifeq2da  4500  ifeq12da  4501  ifclda  4503  ifeqda  4504  ifbothda  4506  2if2  4523  somin1  6090  xpcan  6134  fvmpti  6940  fvmptss  6954  funressn  7106  ovima0  7539  ordsuci  7755  suppssov1  8140  suppssov2  8141  oeoa  8526  oeoe  8528  omabs  8580  eceqoveq  8762  domdifsn  8991  pw2f1olem  9012  mapdom1  9073  imafiOLD  9219  marypha1lem  9339  supval2  9361  infdifsn  9569  ttrcltr  9628  ttrclselem1  9637  carden2b  9882  fidomtri  9908  dfac12lem2  10058  infunsdom1  10125  infunsdom  10126  itunisuc  10332  gchdomtri  10543  fiminre2  12095  xrmax2  13119  xrmin1  13120  ifle  13140  xnn0lem1lt  13187  xmulneg1  13212  xrsupsslem  13250  xrinfmsslem  13251  fzneuz  13553  seqf1olem1  13994  bccmpl  14262  bcval5  14271  bcpasc  14274  bccl  14275  hasheni  14301  hashfn  14328  hashdom  14332  hashdomi  14333  hashge1  14342  hashbc  14406  pfxval0  14630  sumz  15675  sumss  15677  fsumsplitsn  15697  sumsplit  15721  prod1  15900  prodss  15903  fprodsplitsn  15945  fprodle  15952  bitsmod  16396  sadadd2lem2  16410  sadcaddlem  16417  gcddvds  16463  gcdcl  16466  gcdneg  16482  dvdslcm  16558  lcmcl  16561  lcmneg  16563  lcmgcd  16567  lcmfcl  16588  dvdslcmf  16591  pcgcd  16840  pcmpt  16854  pcmpt2  16855  pcprod  16857  fldivp1  16859  prmreclem4  16881  vdwlem6  16948  ramub1lem1  16988  cidpropd  17667  rescabs  17791  lubval  18311  glbval  18324  joinval  18332  meetval  18346  acsexdimd  18516  gsumpropd2lem  18638  gsumval2  18645  mulgfval  19036  f1otrspeq  19413  pmtrfinv  19427  psgnunilem1  19459  gsumval3  19873  ablfac1c  20039  ablfac1eu  20041  mgpress  20122  orngsqr  20834  frlmsslsp  21786  psrbas  21923  resspsrbas  21962  mplmonmul  22024  mplcoe1  22025  mplcoe5  22028  opsrle  22035  opsrbaslem  22037  psrbaspropd  22208  mplbaspropd  22210  mdetdiag  22574  mdetunilem7  22593  mdetunilem9  22595  maducoeval2  22615  madurid  22619  opnnei  23095  restbas  23133  hauspwdom  23476  ptcmplem5  24031  xrsmopn  24788  xrhmeo  24923  lebnum  24941  pcoass  25001  pcorevlem  25003  icombl  25541  ioombl  25542  mbfconstlem  25604  mbfima  25607  i1fd  25658  mbfi1fseqlem5  25696  itg2const2  25718  itg2seq  25719  itg2uba  25720  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  iblss  25782  iblss2  25783  itgss  25789  bddmulibl  25816  coemullem  26225  aaliou2b  26318  isppw2  27092  mule1  27125  ppip1le  27138  dchrelbas3  27215  dchrpt  27244  bposlem3  27263  bposlem5  27265  bposlem6  27266  lgslem4  27277  lgsneg  27298  lgsmod  27300  lgsdilem  27301  lgsdir  27309  lgsdi  27311  lgsne0  27312  lgsquad3  27364  dchrvmasum2if  27474  maxs2  27748  mins1  27749  z12bday  28491  midexlem  28774  colperpex  28815  outpasch  28837  hlpasch  28838  lnopp2hpgb  28845  lmieu  28866  inaghl  28927  cgrg3col4  28935  pthdlem1  29849  nmcfnlbi  32138  elpreq  32613  prssad  32614  prssbd  32615  disjdifprg  32660  disjun0  32680  argcj  32836  f1ocnt  32888  xrge0npcan  33095  psgnfzto1stlem  33176  cyc3genpmlem  33227  cyc3conja  33233  archiabl  33274  erlval  33334  1arithufdlem3  33621  1arithufd  33623  psrmonmul  33709  esplyfval3  33731  resssra  33746  lbslelsp  33757  constrrecl  33929  constrinvcl  33933  constrsqrtcl  33939  1smat1  33964  esumcst  34223  esumrnmpt2  34228  hasheuni  34245  esumcvg  34246  ddemeas  34396  omssubadd  34460  eulerpartlemgc  34522  eulerpartlemb  34528  plymulx  34708  signswmnd  34717  fineqvnttrclselem1  35281  pthhashvtx  35326  erdsze2lem1  35401  mrsubvrs  35720  unblimceq0lem  36782  unbdqndv2lem2  36786  knoppndvlem10  36797  wl-spae  37860  wl-cbvalnaed  37871  wl-nfeqfb  37875  unccur  37938  poimirlem15  37970  poimirlem22  37977  itg2addnclem  38006  itg2addnclem2  38007  iblmulc2nc  38020  ftc1anclem5  38032  ftc1anc  38036  dvasin  38039  areacirclem5  38047  exmid2  38434  3dim1  39927  3dim2  39928  3dim3  39929  3atlem3  39945  3atlem7  39949  lvolnle3at  40042  2lplnja  40079  paddasslem18  40297  lhpexle3lem  40471  4atex  40536  cdlemd5  40662  cdleme16  40745  cdleme20  40784  cdleme21j  40796  cdleme21  40797  cdleme32snaw  40895  cdleme32fvcl  40900  cdleme32le  40907  cdlemeg46gf  40993  cdleme48gfv  40997  cdleme50trn12  41012  cdlemg6  41083  cdlemg7N  41086  cdlemg38  41175  cdlemg46  41195  dibvalrel  41623  dihlss  41710  dihglblem5aN  41752  dihmeetbN  41763  dihmeetALTN  41787  dihatlat  41794  dihatexv  41798  dvh3dim2  41908  dvh3dim3N  41909  lclkrlem2h  41974  mapdh8d  42243  mapdh8g  42245  hdmap11lem2  42302  lcmineqlem23  42504  aks4d1p3  42531  aks4d1p5  42533  aks4d1p7d1  42535  posbezout  42553  aks6d1c2p2  42572  aks6d1c4  42577  aks6d1c5lem1  42589  aks6d1c6lem3  42625  aks6d1c6lem4  42626  bcled  42631  bcle2d  42632  aks6d1c7  42637  grpods  42647  unitscyglem2  42649  unitscyglem4  42651  aks5lem8  42654  dffltz  43081  ttac  43482  pw2f1ocnv  43483  aomclem5  43504  isnumbasgrplem3  43551  iocmbl  43659  oe0suclim  43723  tfsconcatfv  43787  safesnsupfidom1o  43862  safesnsupfilb  43863  r1rankcld  44676  grur1cld  44677  grucollcld  44705  mnuprd  44721  radcnvrat  44759  bccbc  44790  binomcxp  44802  fnchoice  45478  fiiuncl  45514  eliin2f  45552  founiiun0  45638  axccdom  45669  axccd2  45677  fzisoeu  45751  fperiodmul  45755  upbdrech2  45759  fzdifsuc2  45761  uzfissfz  45774  supxrgere  45781  supxrgelem  45785  supxrge  45786  suplesup  45787  infrpge  45799  xrlexaddrp  45800  xralrple2  45802  infxr  45814  infleinflem1  45817  infleinflem2  45818  infleinf  45819  xralrple3  45821  xrralrecnnge  45837  uzublem  45876  supxrmnf2  45879  infxrpnf  45892  infxrpnf2  45909  supminfxr  45910  supminfxr2  45915  pimxrneun  45934  rexanuz2nf  45938  ioondisj2  45941  iccdifprioo  45964  fmul01lt1lem1  46032  fmul01lt1lem2  46033  limciccioolb  46069  lptioo2  46079  lptioo1  46080  limcicciooub  46083  lptre2pt  46086  limcresiooub  46088  limcresioolb  46089  limcleqr  46090  climfveq  46115  climfveqf  46126  limsupubuzlem  46158  limsupubuz  46159  limsupmnfuzlem  46172  limsupre3uzlem  46181  climxrre  46196  limsup10exlem  46218  cnrefiisplem  46275  climxlim2lem  46291  dfxlim2v  46293  xlimliminflimsup  46308  coskpi2  46312  cosknegpi  46315  icccncfext  46333  cncfiooicclem1  46339  cncfiooicc  46340  cncfiooiccre  46341  dvbdfbdioolem2  46375  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnxpaek  46388  dvnprodlem1  46392  dvnprodlem3  46394  volioc  46418  itgioocnicc  46423  iblcncfioo  46424  volico  46429  sublevolico  46430  ismbl3  46432  ovolsplit  46434  volioore  46436  voliooico  46438  voliccico  46445  stoweidlem14  46460  stoweidlem26  46472  stoweidlem28  46474  stoweidlem55  46501  stoweid  46509  stirlinglem5  46524  stirlinglem12  46531  dirkerper  46542  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncf  46553  fourierdlem10  46563  fourierdlem12  46565  fourierdlem24  46577  fourierdlem30  46583  fourierdlem31  46584  fourierdlem32  46585  fourierdlem33  46586  fourierdlem34  46587  fourierdlem35  46588  fourierdlem37  46590  fourierdlem40  46593  fourierdlem41  46594  fourierdlem42  46595  fourierdlem43  46596  fourierdlem44  46597  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem51  46603  fourierdlem54  46606  fourierdlem62  46614  fourierdlem64  46616  fourierdlem65  46617  fourierdlem70  46622  fourierdlem71  46623  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem78  46630  fourierdlem79  46631  fourierdlem80  46632  fourierdlem81  46633  fourierdlem82  46634  fourierdlem92  46644  fourierdlem93  46645  fourierdlem97  46649  fourierdlem101  46653  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem109  46661  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  elaa2lem  46679  etransclem15  46695  etransclem19  46699  etransclem20  46700  etransclem22  46702  etransclem23  46703  etransclem24  46704  etransclem25  46705  etransclem27  46707  etransclem28  46708  etransclem35  46715  etransclem38  46718  qndenserrnbl  46741  ioorrnopn  46751  ioorrnopnxrlem  46752  ioorrnopnxr  46753  prsal  46764  salexct  46780  issalnnd  46791  sge0sn  46825  sge0tsms  46826  sge0cl  46827  sge0f1o  46828  sge0sup  46837  sge0less  46838  sge0pr  46840  sge0prle  46847  sge0le  46853  sge0split  46855  sge0splitmpt  46857  sge0iunmptlemfi  46859  sge0iunmpt  46864  sge0isum  46873  sge0xaddlem1  46879  sge0xadd  46881  sge0gtfsumgt  46889  nnfoctbdjlem  46901  iundjiun  46906  meadjun  46908  ismeannd  46913  voliunsge0lem  46918  meaiuninc3v  46930  caragenfiiuncl  46961  omeiunltfirp  46965  carageniuncl  46969  caragenunicl  46970  isomenndlem  46976  isomennd  46977  hoicvr  46994  ovnssle  47007  ovn0  47012  ovnsubadd  47018  hsphoidmvle2  47031  hoidmvval0b  47036  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1le  47040  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem5  47045  hoidmvle  47046  ovnhoilem1  47047  ovnhoi  47049  ovnlecvr2  47056  hspdifhsp  47062  hoidifhspdmvle  47066  hoiqssbl  47071  hspmbllem1  47072  hspmbllem2  47073  hspmbl  47075  hoimbl  47077  volico2  47087  ovolval2lem  47089  ovnsubadd2lem  47091  ovolval4lem1  47095  ovolval4lem2  47096  ovolval5lem1  47098  vonhoire  47118  iunhoiioo  47122  vonioo  47128  vonicc  47131  vonsn  47137  pimrecltpos  47154  incsmflem  47187  smfpimltxr  47193  smfconst  47195  decsmflem  47212  smfpimgtxr  47226  smfrec  47235  smfpimne2  47286  sharhght  47311  rrx2linest  49230  mofsn2  49332  ipolub00  49480  resccat  49561  initopropdlemlem  49726  prcof1  49875