Theorem pm2.61dan 822

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 416	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61dan.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
4	3	ex 416	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
5	2, 4	pm2.61d 180	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm2.61ddan  823  pm2.61dda  824  nfsb4t  2529  sbal2  2559  pm2.61danel  3074  ifeq1da  4511  ifeq2da  4512  ifeq12da  4513  ifclda  4515  ifeqda  4516  ifbothda  4518  2if2  4535  somin1  6117  xpcan  6158  fvmpti  6970  fvmptss  6984  funressn  7138  ovima0  7571  ordsuci  7787  suppssov1  8172  suppssov2  8173  oeoa  8562  oeoe  8564  omabs  8616  eceqoveq  8799  domdifsn  9028  pw2f1olem  9049  mapdom1  9110  imafiOLD  9256  marypha1lem  9376  supval2  9398  infdifsn  9609  ttrcltr  9668  ttrclselem1  9677  carden2b  9922  fidomtri  9948  dfac12lem2  10098  infunsdom1  10165  infunsdom  10166  itunisuc  10373  gchdomtri  10584  fiminre2  12137  xrmax2  13176  xrmin1  13177  ifle  13197  xnn0lem1lt  13244  xmulneg1  13269  xrsupsslem  13307  xrinfmsslem  13308  fzneuz  13610  seqf1olem1  14051  bccmpl  14319  bcval5  14328  bcpasc  14331  bccl  14332  hasheni  14358  hashfn  14385  hashdom  14389  hashdomi  14390  hashge1  14399  hashbc  14463  pfxval0  14687  sumz  15732  sumss  15734  fsumsplitsn  15754  sumsplit  15778  prod1  15957  prodss  15960  fprodsplitsn  16002  fprodle  16009  bitsmod  16453  sadadd2lem2  16467  sadcaddlem  16474  gcddvds  16520  gcdcl  16523  gcdneg  16539  dvdslcm  16615  lcmcl  16618  lcmneg  16620  lcmgcd  16624  lcmfcl  16645  dvdslcmf  16648  pcgcd  16897  pcmpt  16911  pcmpt2  16912  pcprod  16914  fldivp1  16916  prmreclem4  16938  vdwlem6  17005  ramub1lem1  17045  cidpropd  17725  rescabs  17849  lubval  18369  glbval  18382  joinval  18390  meetval  18404  acsexdimd  18574  gsumpropd2lem  18696  gsumval2  18703  mulgfval  19094  f1otrspeq  19470  pmtrfinv  19484  psgnunilem1  19516  gsumval3  19930  ablfac1c  20096  ablfac1eu  20098  mgpress  20179  orngsqr  20895  frlmsslsp  21828  psrbas  21966  resspsrbas  22005  mplmonmul  22069  mplcoe1  22070  mplcoe5  22073  opsrle  22080  opsrbaslem  22082  psrbaspropd  22276  mplbaspropd  22278  mdetdiag  22639  mdetunilem7  22658  mdetunilem9  22660  maducoeval2  22680  madurid  22684  opnnei  23160  restbas  23198  hauspwdom  23541  ptcmplem5  24096  xrsmopn  24853  xrhmeo  24988  lebnum  25006  pcoass  25066  pcorevlem  25068  icombl  25606  ioombl  25607  mbfconstlem  25669  mbfima  25672  i1fd  25723  mbfi1fseqlem5  25761  itg2const2  25783  itg2seq  25784  itg2uba  25785  itg2splitlem  25790  itg2split  25791  itg2monolem1  25792  itg2gt0  25802  itg2cnlem1  25803  itg2cnlem2  25804  iblss  25847  iblss2  25848  itgss  25854  bddmulibl  25881  coemullem  26290  aaliou2b  26382  isppw2  27156  mule1  27189  ppip1le  27202  dchrelbas3  27279  dchrpt  27308  bposlem3  27327  bposlem5  27329  bposlem6  27330  lgslem4  27341  lgsneg  27362  lgsmod  27364  lgsdilem  27365  lgsdir  27373  lgsdi  27375  lgsne0  27376  lgsquad3  27428  dchrvmasum2if  27538  maxs2  27811  mins1  27812  z12bday  28555  midexlem  28838  colperpex  28879  outpasch  28901  hlpasch  28902  lnopp2hpgb  28909  lmieu  28930  inaghl  28991  cgrg3col4  28999  pthdlem1  29912  nmcfnlbi  32201  elpreq  32676  prssad  32677  prssbd  32678  disjdifprg  32724  disjun0  32744  argcj  32900  f1ocnt  32952  xrge0npcan  33159  psgnfzto1stlem  33241  cyc3genpmlem  33292  cyc3conja  33298  archiabl  33339  erlval  33400  1arithufdlem3  33703  1arithufd  33705  psrmonmul  33808  esplyfval3  33830  resssra  33845  lbslelsp  33856  constrrecl  34027  constrinvcl  34031  constrsqrtcl  34037  1smat1  34062  esumcst  34321  esumrnmpt2  34326  hasheuni  34343  esumcvg  34344  ddemeas  34494  omssubadd  34558  eulerpartlemgc  34620  eulerpartlemb  34626  plymulx  34806  signswmnd  34815  fineqvnttrclselem1  35381  pthhashvtx  35442  erdsze2lem1  35517  mrsubvrs  35836  unblimceq0lem  36908  unbdqndv2lem2  36912  knoppndvlem10  36923  wl-spae  37988  wl-cbvalnaed  37999  wl-nfeqfb  38003  unccur  38066  poimirlem15  38098  poimirlem22  38105  itg2addnclem  38134  itg2addnclem2  38135  iblmulc2nc  38148  ftc1anclem5  38160  ftc1anc  38164  dvasin  38167  areacirclem5  38175  exmid2  38562  3dim1  40055  3dim2  40056  3dim3  40057  3atlem3  40073  3atlem7  40077  lvolnle3at  40170  2lplnja  40207  paddasslem18  40425  lhpexle3lem  40599  4atex  40664  cdlemd5  40790  cdleme16  40873  cdleme20  40912  cdleme21j  40924  cdleme21  40925  cdleme32snaw  41023  cdleme32fvcl  41028  cdleme32le  41035  cdlemeg46gf  41121  cdleme48gfv  41125  cdleme50trn12  41140  cdlemg6  41211  cdlemg7N  41214  cdlemg38  41303  cdlemg46  41323  dibvalrel  41751  dihlss  41838  dihglblem5aN  41880  dihmeetbN  41891  dihmeetALTN  41915  dihatlat  41922  dihatexv  41926  dvh3dim2  42036  dvh3dim3N  42037  lclkrlem2h  42102  mapdh8d  42371  mapdh8g  42373  hdmap11lem2  42430  lcmineqlem23  42632  aks4d1p3  42659  aks4d1p5  42661  aks4d1p7d1  42663  posbezout  42681  aks6d1c2p2  42700  aks6d1c4  42705  aks6d1c5lem1  42717  aks6d1c6lem3  42753  aks6d1c6lem4  42754  bcled  42759  bcle2d  42760  aks6d1c7  42765  grpods  42775  unitscyglem2  42777  unitscyglem4  42779  aks5lem8  42782  dffltz  43180  ttac  43577  pw2f1ocnv  43578  aomclem5  43599  isnumbasgrplem3  43646  iocmbl  43754  oe0suclim  43818  tfsconcatfv  43882  safesnsupfidom1o  43957  safesnsupfilb  43958  r1rankcld  44771  grur1cld  44772  grucollcld  44800  mnuprd  44816  radcnvrat  44854  bccbc  44885  binomcxp  44897  fnchoice  45573  fiiuncl  45609  eliin2f  45646  founiiun0  45732  axccdom  45762  axccd2  45769  fzisoeu  45843  fperiodmul  45847  upbdrech2  45851  fzdifsuc2  45853  uzfissfz  45866  supxrgere  45873  supxrgelem  45877  supxrge  45878  suplesup  45879  infrpge  45891  xrlexaddrp  45892  xralrple2  45894  infxr  45906  infleinflem1  45909  infleinflem2  45910  infleinf  45911  xralrple3  45913  xrralrecnnge  45929  uzublem  45968  supxrmnf2  45971  infxrpnf  45984  infxrpnf2  46001  supminfxr  46002  supminfxr2  46007  pimxrneun  46026  rexanuz2nf  46030  ioondisj2  46033  iccdifprioo  46056  fmul01lt1lem1  46124  fmul01lt1lem2  46125  limciccioolb  46161  lptioo2  46171  lptioo1  46172  limcicciooub  46175  lptre2pt  46178  limcresiooub  46180  limcresioolb  46181  limcleqr  46182  climfveq  46207  climfveqf  46218  limsupubuzlem  46250  limsupubuz  46251  limsupmnfuzlem  46264  limsupre3uzlem  46273  climxrre  46288  limsup10exlem  46310  cnrefiisplem  46367  climxlim2lem  46383  dfxlim2v  46385  xlimliminflimsup  46400  coskpi2  46404  cosknegpi  46407  icccncfext  46425  cncfiooicclem1  46431  cncfiooicc  46432  cncfiooiccre  46433  dvbdfbdioolem2  46467  ioodvbdlimc1lem1  46469  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnxpaek  46480  dvnprodlem1  46484  dvnprodlem3  46486  volioc  46510  itgioocnicc  46515  iblcncfioo  46516  volico  46521  sublevolico  46522  ismbl3  46524  ovolsplit  46526  volioore  46528  voliooico  46530  voliccico  46537  stoweidlem14  46552  stoweidlem26  46564  stoweidlem28  46566  stoweidlem55  46593  stoweid  46601  stirlinglem5  46616  stirlinglem12  46623  dirkerper  46634  dirkertrigeqlem3  46638  dirkertrigeq  46639  dirkercncflem1  46641  dirkercncflem2  46642  dirkercncf  46645  fourierdlem10  46655  fourierdlem12  46657  fourierdlem24  46669  fourierdlem30  46675  fourierdlem31  46676  fourierdlem32  46677  fourierdlem33  46678  fourierdlem34  46679  fourierdlem35  46680  fourierdlem37  46682  fourierdlem40  46685  fourierdlem41  46686  fourierdlem42  46687  fourierdlem43  46688  fourierdlem44  46689  fourierdlem46  46690  fourierdlem48  46692  fourierdlem49  46693  fourierdlem51  46695  fourierdlem54  46698  fourierdlem62  46706  fourierdlem64  46708  fourierdlem65  46709  fourierdlem70  46714  fourierdlem71  46715  fourierdlem73  46717  fourierdlem74  46718  fourierdlem75  46719  fourierdlem78  46722  fourierdlem79  46723  fourierdlem80  46724  fourierdlem81  46725  fourierdlem82  46726  fourierdlem92  46736  fourierdlem93  46737  fourierdlem97  46741  fourierdlem101  46745  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem109  46753  fourierdlem114  46758  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  elaa2lem  46771  etransclem15  46787  etransclem19  46791  etransclem20  46792  etransclem22  46794  etransclem23  46795  etransclem24  46796  etransclem25  46797  etransclem27  46799  etransclem28  46800  etransclem35  46807  etransclem38  46810  qndenserrnbl  46833  ioorrnopn  46843  ioorrnopnxrlem  46844  ioorrnopnxr  46845  prsal  46856  salexct  46872  issalnnd  46883  sge0sn  46917  sge0tsms  46918  sge0cl  46919  sge0f1o  46920  sge0sup  46929  sge0less  46930  sge0pr  46932  sge0prle  46939  sge0le  46945  sge0split  46947  sge0splitmpt  46949  sge0iunmptlemfi  46951  sge0iunmpt  46956  sge0isum  46965  sge0xaddlem1  46971  sge0xadd  46973  sge0gtfsumgt  46981  nnfoctbdjlem  46993  iundjiun  46998  meadjun  47000  ismeannd  47005  voliunsge0lem  47010  meaiuninc3v  47022  caragenfiiuncl  47053  omeiunltfirp  47057  carageniuncl  47061  caragenunicl  47062  isomenndlem  47068  isomennd  47069  hoicvr  47086  ovnssle  47099  ovn0  47104  ovnsubadd  47110  hsphoidmvle2  47123  hoidmvval0b  47128  hoidmv1lelem1  47129  hoidmv1lelem2  47130  hoidmv1le  47132  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem5  47137  hoidmvle  47138  ovnhoilem1  47139  ovnhoi  47141  ovnlecvr2  47148  hspdifhsp  47154  hoidifhspdmvle  47158  hoiqssbl  47163  hspmbllem1  47164  hspmbllem2  47165  hspmbl  47167  hoimbl  47169  volico2  47179  ovolval2lem  47181  ovnsubadd2lem  47183  ovolval4lem1  47187  ovolval4lem2  47188  ovolval5lem1  47190  vonhoire  47210  iunhoiioo  47214  vonioo  47220  vonicc  47223  vonsn  47229  pimrecltpos  47246  incsmflem  47279  smfpimltxr  47285  smfconst  47287  decsmflem  47304  smfpimgtxr  47318  smfrec  47327  smfpimne2  47378  sharhght  47403  rrx2linest  49328  mofsn2  49430  ipolub00  49578  resccat  49659  initopropdlemlem  49824  prcof1  49973