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

This theorem is referenced by:  pm2.61ddan  814  pm2.61dda  815  nfsb4t  2502  sbal2  2533  pm2.61danel  3060  ifeq1da  4470  ifeq2da  4471  ifeq12da  4472  ifclda  4474  ifeqda  4475  ifbothda  4477  2if2  4494  somin1  5998  xpcan  6039  fvmpti  6817  fvmptss  6830  funressn  6974  ovima0  7387  oeoa  8325  oeoe  8327  omabs  8376  eceqoveq  8504  domdifsn  8728  pw2f1olem  8749  mapdom1  8811  imafi  8853  marypha1lem  9049  supval2  9071  infdifsn  9272  trpredlem1  9332  carden2b  9583  fidomtri  9609  dfac12lem2  9758  infunsdom1  9827  infunsdom  9828  itunisuc  10033  gchdomtri  10243  fiminre2  11780  xrmax2  12766  xrmin1  12767  ifle  12787  xnn0lem1lt  12834  xmulneg1  12859  xrsupsslem  12897  xrinfmsslem  12898  fzneuz  13193  seqf1olem1  13615  bccmpl  13875  bcval5  13884  bcpasc  13887  bccl  13888  hasheni  13914  hashfn  13942  hashdom  13946  hashdomi  13947  hashge1  13956  hashbc  14017  pfxval0  14241  sumz  15286  sumss  15288  fsumsplitsn  15308  sumsplit  15332  prod1  15506  prodss  15509  fprodsplitsn  15551  fprodle  15558  bitsmod  15995  sadadd2lem2  16009  sadcaddlem  16016  gcddvds  16062  gcdcl  16065  gcdneg  16081  dvdslcm  16155  lcmcl  16158  lcmneg  16160  lcmgcd  16164  lcmfcl  16185  dvdslcmf  16188  pcgcd  16431  pcmpt  16445  pcmpt2  16446  pcprod  16448  fldivp1  16450  prmreclem4  16472  vdwlem6  16539  ramub1lem1  16579  cidpropd  17213  rescabs  17339  lubval  17862  glbval  17875  joinval  17883  meetval  17897  acsexdimd  18065  gsumpropd2lem  18151  gsumval2  18158  mulgfval  18490  f1otrspeq  18839  pmtrfinv  18853  psgnunilem1  18885  gsumval3  19292  ablfac1c  19458  ablfac1eu  19460  mgpress  19515  frlmsslsp  20758  psrbas  20903  resspsrbas  20940  mplmonmul  20993  mplcoe1  20994  mplcoe5  20997  opsrle  21004  opsrbaslem  21006  psrbaspropd  21156  mplbaspropd  21158  mdetdiag  21496  mdetunilem7  21515  mdetunilem9  21517  maducoeval2  21537  madurid  21541  opnnei  22017  restbas  22055  hauspwdom  22398  ptcmplem5  22953  xrsmopn  23709  xrhmeo  23843  lebnum  23861  pcoass  23921  pcorevlem  23923  icombl  24461  ioombl  24462  mbfconstlem  24524  mbfima  24527  i1fd  24578  mbfi1fseqlem5  24617  itg2const2  24639  itg2seq  24640  itg2uba  24641  itg2splitlem  24646  itg2split  24647  itg2monolem1  24648  itg2gt0  24658  itg2cnlem1  24659  itg2cnlem2  24660  iblss  24702  iblss2  24703  itgss  24709  bddmulibl  24736  coemullem  25144  aaliou2b  25234  isppw2  25997  mule1  26030  ppip1le  26043  dchrelbas3  26119  dchrpt  26148  bposlem3  26167  bposlem5  26169  bposlem6  26170  lgslem4  26181  lgsneg  26202  lgsmod  26204  lgsdilem  26205  lgsdir  26213  lgsdi  26215  lgsne0  26216  lgsquad3  26268  dchrvmasum2if  26378  midexlem  26783  colperpex  26824  outpasch  26846  hlpasch  26847  lnopp2hpgb  26854  lmieu  26875  inaghl  26936  cgrg3col4  26944  pthdlem1  27853  nmcfnlbi  30133  elpreq  30597  disjdifprg  30633  disjun0  30653  f1ocnt  30843  xrge0npcan  31022  psgnfzto1stlem  31086  cyc3genpmlem  31137  cyc3conja  31143  archiabl  31171  orngsqr  31222  1smat1  31468  esumcst  31743  esumrnmpt2  31748  hasheuni  31765  esumcvg  31766  ddemeas  31916  omssubadd  31979  eulerpartlemgc  32041  eulerpartlemb  32047  plymulx  32239  signswmnd  32248  pthhashvtx  32802  erdsze2lem1  32878  mrsubvrs  33197  ttrcltr  33515  unblimceq0lem  34423  unbdqndv2lem2  34427  knoppndvlem10  34438  wl-spae  35417  wl-cbvalnaed  35428  wl-nfeqfb  35432  unccur  35497  poimirlem15  35529  poimirlem22  35536  itg2addnclem  35565  itg2addnclem2  35566  iblmulc2nc  35579  ftc1anclem5  35591  ftc1anc  35595  dvasin  35598  areacirclem5  35606  exmid2  35994  3dim1  37218  3dim2  37219  3dim3  37220  3atlem3  37236  3atlem7  37240  lvolnle3at  37333  2lplnja  37370  paddasslem18  37588  lhpexle3lem  37762  4atex  37827  cdlemd5  37953  cdleme16  38036  cdleme20  38075  cdleme21j  38087  cdleme21  38088  cdleme32snaw  38186  cdleme32fvcl  38191  cdleme32le  38198  cdlemeg46gf  38284  cdleme48gfv  38288  cdleme50trn12  38303  cdlemg6  38374  cdlemg7N  38377  cdlemg38  38466  cdlemg46  38486  dibvalrel  38914  dihlss  39001  dihglblem5aN  39043  dihmeetbN  39054  dihmeetALTN  39078  dihatlat  39085  dihatexv  39089  dvh3dim2  39199  dvh3dim3N  39200  lclkrlem2h  39265  mapdh8d  39534  mapdh8g  39536  hdmap11lem2  39593  lcmineqlem23  39793  aks4d1p3  39819  metakunt23  39869  metakunt24  39870  metakunt29  39875  metakunt30  39876  metakunt31  39877  dffltz  40174  ttac  40561  pw2f1ocnv  40562  aomclem5  40586  isnumbasgrplem3  40633  iocmbl  40747  r1rankcld  41522  grur1cld  41523  grucollcld  41551  mnuprd  41567  radcnvrat  41605  bccbc  41636  binomcxp  41648  fnchoice  42245  fiiuncl  42286  eliin2f  42327  founiiun0  42401  axccdom  42435  axccd2  42442  fzisoeu  42512  fperiodmul  42516  upbdrech2  42520  fzdifsuc2  42522  uzfissfz  42538  supxrgere  42545  supxrgelem  42549  supxrge  42550  suplesup  42551  infrpge  42563  xrlexaddrp  42564  xralrple2  42566  infxr  42579  infleinflem1  42582  infleinflem2  42583  infleinf  42584  xralrple3  42586  xrralrecnnge  42603  uzublem  42643  supxrmnf2  42646  infxrpnf  42660  infxrpnf2  42678  supminfxr  42679  supminfxr2  42684  ioondisj2  42706  iccdifprioo  42729  fmul01lt1lem1  42800  fmul01lt1lem2  42801  limciccioolb  42837  lptioo2  42847  lptioo1  42848  limcicciooub  42853  lptre2pt  42856  limcresiooub  42858  limcresioolb  42859  limcleqr  42860  climfveq  42885  climfveqf  42896  limsupubuzlem  42928  limsupubuz  42929  limsupmnfuzlem  42942  limsupre3uzlem  42951  climxrre  42966  limsup10exlem  42988  cnrefiisplem  43045  climxlim2lem  43061  dfxlim2v  43063  xlimliminflimsup  43078  coskpi2  43082  cosknegpi  43085  icccncfext  43103  cncfiooicclem1  43109  cncfiooicc  43110  cncfiooiccre  43111  dvbdfbdioolem2  43145  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  dvnxpaek  43158  dvnprodlem1  43162  dvnprodlem3  43164  volioc  43188  itgioocnicc  43193  iblcncfioo  43194  volico  43199  sublevolico  43200  ismbl3  43202  ovolsplit  43204  volioore  43206  voliooico  43208  voliccico  43215  stoweidlem14  43230  stoweidlem26  43242  stoweidlem28  43244  stoweidlem55  43271  stoweid  43279  stirlinglem5  43294  stirlinglem12  43301  dirkerper  43312  dirkertrigeqlem3  43316  dirkertrigeq  43317  dirkercncflem1  43319  dirkercncflem2  43320  dirkercncf  43323  fourierdlem10  43333  fourierdlem12  43335  fourierdlem24  43347  fourierdlem30  43353  fourierdlem31  43354  fourierdlem32  43355  fourierdlem33  43356  fourierdlem34  43357  fourierdlem35  43358  fourierdlem37  43360  fourierdlem40  43363  fourierdlem41  43364  fourierdlem42  43365  fourierdlem43  43366  fourierdlem44  43367  fourierdlem46  43368  fourierdlem48  43370  fourierdlem49  43371  fourierdlem51  43373  fourierdlem54  43376  fourierdlem62  43384  fourierdlem64  43386  fourierdlem65  43387  fourierdlem70  43392  fourierdlem71  43393  fourierdlem73  43395  fourierdlem74  43396  fourierdlem75  43397  fourierdlem78  43400  fourierdlem79  43401  fourierdlem80  43402  fourierdlem81  43403  fourierdlem82  43404  fourierdlem92  43414  fourierdlem93  43415  fourierdlem97  43419  fourierdlem101  43423  fourierdlem102  43424  fourierdlem103  43425  fourierdlem104  43426  fourierdlem109  43431  fourierdlem114  43436  sqwvfoura  43444  sqwvfourb  43445  fourierswlem  43446  fouriersw  43447  elaa2lem  43449  etransclem15  43465  etransclem19  43469  etransclem20  43470  etransclem22  43472  etransclem23  43473  etransclem24  43474  etransclem25  43475  etransclem27  43477  etransclem28  43478  etransclem35  43485  etransclem38  43488  qndenserrnbl  43511  ioorrnopn  43521  ioorrnopnxrlem  43522  ioorrnopnxr  43523  prsal  43534  salexct  43548  issalnnd  43559  sge0sn  43592  sge0tsms  43593  sge0cl  43594  sge0f1o  43595  sge0sup  43604  sge0less  43605  sge0pr  43607  sge0prle  43614  sge0le  43620  sge0split  43622  sge0splitmpt  43624  sge0iunmptlemfi  43626  sge0iunmpt  43631  sge0isum  43640  sge0xaddlem1  43646  sge0xadd  43648  sge0gtfsumgt  43656  nnfoctbdjlem  43668  iundjiun  43673  meadjun  43675  ismeannd  43680  voliunsge0lem  43685  meaiuninc3v  43697  caragenfiiuncl  43728  omeiunltfirp  43732  carageniuncl  43736  caragenunicl  43737  isomenndlem  43743  isomennd  43744  hoicvr  43761  ovnssle  43774  ovn0  43779  ovnsubadd  43785  hsphoidmvle2  43798  hoidmvval0b  43803  hoidmv1lelem1  43804  hoidmv1lelem2  43805  hoidmv1le  43807  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvlelem5  43812  hoidmvle  43813  ovnhoilem1  43814  ovnhoi  43816  ovnlecvr2  43823  hspdifhsp  43829  hoidifhspdmvle  43833  hoiqssbl  43838  hspmbllem1  43839  hspmbllem2  43840  hspmbl  43842  hoimbl  43844  volico2  43854  ovolval2lem  43856  ovnsubadd2lem  43858  ovolval4lem1  43862  ovolval4lem2  43863  ovolval5lem1  43865  vonhoire  43885  iunhoiioo  43889  vonioo  43895  vonicc  43898  vonsn  43904  pimrecltpos  43918  incsmflem  43949  smfpimltxr  43955  smfconst  43957  decsmflem  43973  smfpimgtxr  43987  smfrec  43995  sharhght  44053  rrx2linest  45761  mofsn2  45845  ipolub00  45952