Theorem pm2.61dan 811

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

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

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 206  df-an 398

This theorem is referenced by:  pm2.61ddan  812  pm2.61dda  813  nfsb4t  2502  sbal2  2533  pm2.61danel  3061  ifeq1da  4508  ifeq2da  4509  ifeq12da  4510  ifclda  4512  ifeqda  4513  ifbothda  4515  2if2  4532  somin1  6077  xpcan  6118  fvmpti  6934  fvmptss  6947  funressn  7091  ovima0  7517  ordsuci  7725  oeoa  8503  oeoe  8505  omabs  8556  eceqoveq  8686  domdifsn  8923  pw2f1olem  8945  mapdom1  9011  imafi  9044  marypha1lem  9294  supval2  9316  infdifsn  9518  ttrcltr  9577  ttrclselem1  9586  carden2b  9828  fidomtri  9854  dfac12lem2  10005  infunsdom1  10074  infunsdom  10075  itunisuc  10280  gchdomtri  10490  fiminre2  12028  xrmax2  13015  xrmin1  13016  ifle  13036  xnn0lem1lt  13083  xmulneg1  13108  xrsupsslem  13146  xrinfmsslem  13147  fzneuz  13442  seqf1olem1  13867  bccmpl  14128  bcval5  14137  bcpasc  14140  bccl  14141  hasheni  14167  hashfn  14194  hashdom  14198  hashdomi  14199  hashge1  14208  hashbc  14269  pfxval0  14487  sumz  15533  sumss  15535  fsumsplitsn  15555  sumsplit  15579  prod1  15753  prodss  15756  fprodsplitsn  15798  fprodle  15805  bitsmod  16242  sadadd2lem2  16256  sadcaddlem  16263  gcddvds  16309  gcdcl  16312  gcdneg  16328  dvdslcm  16400  lcmcl  16403  lcmneg  16405  lcmgcd  16409  lcmfcl  16430  dvdslcmf  16433  pcgcd  16676  pcmpt  16690  pcmpt2  16691  pcprod  16693  fldivp1  16695  prmreclem4  16717  vdwlem6  16784  ramub1lem1  16824  cidpropd  17516  rescabs  17644  rescabsOLD  17645  lubval  18171  glbval  18184  joinval  18192  meetval  18206  acsexdimd  18374  gsumpropd2lem  18460  gsumval2  18467  mulgfval  18798  f1otrspeq  19151  pmtrfinv  19165  psgnunilem1  19197  gsumval3  19602  ablfac1c  19768  ablfac1eu  19770  mgpress  19829  mgpressOLD  19830  frlmsslsp  21108  psrbas  21252  resspsrbas  21289  mplmonmul  21342  mplcoe1  21343  mplcoe5  21346  opsrle  21353  opsrbaslem  21355  opsrbaslemOLD  21356  psrbaspropd  21511  mplbaspropd  21513  mdetdiag  21853  mdetunilem7  21872  mdetunilem9  21874  maducoeval2  21894  madurid  21898  opnnei  22376  restbas  22414  hauspwdom  22757  ptcmplem5  23312  xrsmopn  24080  xrhmeo  24214  lebnum  24232  pcoass  24292  pcorevlem  24294  icombl  24833  ioombl  24834  mbfconstlem  24896  mbfima  24899  i1fd  24950  mbfi1fseqlem5  24989  itg2const2  25011  itg2seq  25012  itg2uba  25013  itg2splitlem  25018  itg2split  25019  itg2monolem1  25020  itg2gt0  25030  itg2cnlem1  25031  itg2cnlem2  25032  iblss  25074  iblss2  25075  itgss  25081  bddmulibl  25108  coemullem  25516  aaliou2b  25606  isppw2  26369  mule1  26402  ppip1le  26415  dchrelbas3  26491  dchrpt  26520  bposlem3  26539  bposlem5  26541  bposlem6  26542  lgslem4  26553  lgsneg  26574  lgsmod  26576  lgsdilem  26577  lgsdir  26585  lgsdi  26587  lgsne0  26588  lgsquad3  26640  dchrvmasum2if  26750  midexlem  27341  colperpex  27382  outpasch  27404  hlpasch  27405  lnopp2hpgb  27412  lmieu  27433  inaghl  27494  cgrg3col4  27502  pthdlem1  28421  nmcfnlbi  30701  elpreq  31163  disjdifprg  31199  disjun0  31219  f1ocnt  31408  xrge0npcan  31588  psgnfzto1stlem  31652  cyc3genpmlem  31703  cyc3conja  31709  archiabl  31737  orngsqr  31801  1smat1  32050  esumcst  32327  esumrnmpt2  32332  hasheuni  32349  esumcvg  32350  ddemeas  32500  omssubadd  32565  eulerpartlemgc  32627  eulerpartlemb  32633  plymulx  32825  signswmnd  32834  pthhashvtx  33386  erdsze2lem1  33462  mrsubvrs  33781  unblimceq0lem  34823  unbdqndv2lem2  34827  knoppndvlem10  34838  wl-spae  35834  wl-cbvalnaed  35845  wl-nfeqfb  35849  unccur  35916  poimirlem15  35948  poimirlem22  35955  itg2addnclem  35984  itg2addnclem2  35985  iblmulc2nc  35998  ftc1anclem5  36010  ftc1anc  36014  dvasin  36017  areacirclem5  36025  exmid2  36413  3dim1  37786  3dim2  37787  3dim3  37788  3atlem3  37804  3atlem7  37808  lvolnle3at  37901  2lplnja  37938  paddasslem18  38156  lhpexle3lem  38330  4atex  38395  cdlemd5  38521  cdleme16  38604  cdleme20  38643  cdleme21j  38655  cdleme21  38656  cdleme32snaw  38754  cdleme32fvcl  38759  cdleme32le  38766  cdlemeg46gf  38852  cdleme48gfv  38856  cdleme50trn12  38871  cdlemg6  38942  cdlemg7N  38945  cdlemg38  39034  cdlemg46  39054  dibvalrel  39482  dihlss  39569  dihglblem5aN  39611  dihmeetbN  39622  dihmeetALTN  39646  dihatlat  39653  dihatexv  39657  dvh3dim2  39767  dvh3dim3N  39768  lclkrlem2h  39833  mapdh8d  40102  mapdh8g  40104  hdmap11lem2  40161  lcmineqlem23  40364  aks4d1p3  40391  aks4d1p5  40393  aks4d1p7d1  40395  aks6d1c2p2  40405  metakunt23  40455  metakunt24  40456  metakunt29  40461  metakunt30  40462  metakunt31  40463  dffltz  40784  ttac  41172  pw2f1ocnv  41173  aomclem5  41197  isnumbasgrplem3  41244  iocmbl  41359  safesnsupfidom1o  41398  safesnsupfilb  41399  r1rankcld  42222  grur1cld  42223  grucollcld  42251  mnuprd  42267  radcnvrat  42305  bccbc  42336  binomcxp  42348  fnchoice  42945  fiiuncl  42985  eliin2f  43026  founiiun0  43107  axccdom  43141  axccd2  43149  fzisoeu  43226  fperiodmul  43230  upbdrech2  43234  fzdifsuc2  43236  uzfissfz  43252  supxrgere  43259  supxrgelem  43263  supxrge  43264  suplesup  43265  infrpge  43277  xrlexaddrp  43278  xralrple2  43280  infxr  43293  infleinflem1  43296  infleinflem2  43297  infleinf  43298  xralrple3  43300  xrralrecnnge  43317  uzublem  43357  supxrmnf2  43360  infxrpnf  43373  infxrpnf2  43390  supminfxr  43391  supminfxr2  43396  pimxrneun  43416  ioondisj2  43419  iccdifprioo  43442  fmul01lt1lem1  43513  fmul01lt1lem2  43514  limciccioolb  43550  lptioo2  43560  lptioo1  43561  limcicciooub  43566  lptre2pt  43569  limcresiooub  43571  limcresioolb  43572  limcleqr  43573  climfveq  43598  climfveqf  43609  limsupubuzlem  43641  limsupubuz  43642  limsupmnfuzlem  43655  limsupre3uzlem  43664  climxrre  43679  limsup10exlem  43701  cnrefiisplem  43758  climxlim2lem  43774  dfxlim2v  43776  xlimliminflimsup  43791  coskpi2  43795  cosknegpi  43798  icccncfext  43816  cncfiooicclem1  43822  cncfiooicc  43823  cncfiooiccre  43824  dvbdfbdioolem2  43858  ioodvbdlimc1lem1  43860  ioodvbdlimc1lem2  43861  ioodvbdlimc2lem  43863  dvnxpaek  43871  dvnprodlem1  43875  dvnprodlem3  43877  volioc  43901  itgioocnicc  43906  iblcncfioo  43907  volico  43912  sublevolico  43913  ismbl3  43915  ovolsplit  43917  volioore  43919  voliooico  43921  voliccico  43928  stoweidlem14  43943  stoweidlem26  43955  stoweidlem28  43957  stoweidlem55  43984  stoweid  43992  stirlinglem5  44007  stirlinglem12  44014  dirkerper  44025  dirkertrigeqlem3  44029  dirkertrigeq  44030  dirkercncflem1  44032  dirkercncflem2  44033  dirkercncf  44036  fourierdlem10  44046  fourierdlem12  44048  fourierdlem24  44060  fourierdlem30  44066  fourierdlem31  44067  fourierdlem32  44068  fourierdlem33  44069  fourierdlem34  44070  fourierdlem35  44071  fourierdlem37  44073  fourierdlem40  44076  fourierdlem41  44077  fourierdlem42  44078  fourierdlem43  44079  fourierdlem44  44080  fourierdlem46  44081  fourierdlem48  44083  fourierdlem49  44084  fourierdlem51  44086  fourierdlem54  44089  fourierdlem62  44097  fourierdlem64  44099  fourierdlem65  44100  fourierdlem70  44105  fourierdlem71  44106  fourierdlem73  44108  fourierdlem74  44109  fourierdlem75  44110  fourierdlem78  44113  fourierdlem79  44114  fourierdlem80  44115  fourierdlem81  44116  fourierdlem82  44117  fourierdlem92  44127  fourierdlem93  44128  fourierdlem97  44132  fourierdlem101  44136  fourierdlem102  44137  fourierdlem103  44138  fourierdlem104  44139  fourierdlem109  44144  fourierdlem114  44149  sqwvfoura  44157  sqwvfourb  44158  fourierswlem  44159  fouriersw  44160  elaa2lem  44162  etransclem15  44178  etransclem19  44182  etransclem20  44183  etransclem22  44185  etransclem23  44186  etransclem24  44187  etransclem25  44188  etransclem27  44190  etransclem28  44191  etransclem35  44198  etransclem38  44201  qndenserrnbl  44224  ioorrnopn  44234  ioorrnopnxrlem  44235  ioorrnopnxr  44236  prsal  44247  salexct  44261  issalnnd  44272  sge0sn  44306  sge0tsms  44307  sge0cl  44308  sge0f1o  44309  sge0sup  44318  sge0less  44319  sge0pr  44321  sge0prle  44328  sge0le  44334  sge0split  44336  sge0splitmpt  44338  sge0iunmptlemfi  44340  sge0iunmpt  44345  sge0isum  44354  sge0xaddlem1  44360  sge0xadd  44362  sge0gtfsumgt  44370  nnfoctbdjlem  44382  iundjiun  44387  meadjun  44389  ismeannd  44394  voliunsge0lem  44399  meaiuninc3v  44411  caragenfiiuncl  44442  omeiunltfirp  44446  carageniuncl  44450  caragenunicl  44451  isomenndlem  44457  isomennd  44458  hoicvr  44475  ovnssle  44488  ovn0  44493  ovnsubadd  44499  hsphoidmvle2  44512  hoidmvval0b  44517  hoidmv1lelem1  44518  hoidmv1lelem2  44519  hoidmv1le  44521  hoidmvlelem2  44523  hoidmvlelem3  44524  hoidmvlelem5  44526  hoidmvle  44527  ovnhoilem1  44528  ovnhoi  44530  ovnlecvr2  44537  hspdifhsp  44543  hoidifhspdmvle  44547  hoiqssbl  44552  hspmbllem1  44553  hspmbllem2  44554  hspmbl  44556  hoimbl  44558  volico2  44568  ovolval2lem  44570  ovnsubadd2lem  44572  ovolval4lem1  44576  ovolval4lem2  44577  ovolval5lem1  44579  vonhoire  44599  iunhoiioo  44603  vonioo  44609  vonicc  44612  vonsn  44618  pimrecltpos  44635  incsmflem  44668  smfpimltxr  44674  smfconst  44676  decsmflem  44693  smfpimgtxr  44707  smfrec  44716  smfpimne2  44767  sharhght  44784  rrx2linest  46506  mofsn2  46590  ipolub00  46697