Theorem pm2.61dan 809

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

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

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 208  df-an 397

This theorem is referenced by:  pm2.61ddan  810  pm2.61dda  811  nfsb4t  2493  sbal2  2526  sbal2OLD  2527  nfsb4tALT  2558  pm2.61danel  3104  ifeq1da  4415  ifeq2da  4416  ifeq12da  4417  ifclda  4419  ifeqda  4420  ifbothda  4422  2if2  4438  somin1  5874  xpcan  5914  fvmpti  6639  fvmptss  6651  funressn  6789  ovima0  7188  oeoa  8078  oeoe  8080  omabs  8129  eceqoveq  8257  domdifsn  8452  pw2f1olem  8473  mapdom1  8534  marypha1lem  8748  supval2  8770  infdifsn  8971  carden2b  9247  fidomtri  9273  dfac12lem2  9421  infunsdom1  9486  infunsdom  9487  itunisuc  9692  gchdomtri  9902  xrmax2  12424  xrmin1  12425  ifle  12445  xnn0lem1lt  12492  xmulneg1  12517  xrsupsslem  12555  xrinfmsslem  12556  fzneuz  12843  seqf1olem1  13264  bccmpl  13524  bcval5  13533  bcpasc  13536  bccl  13537  hasheni  13563  hashfn  13589  hashdom  13593  hashdomi  13594  hashge1  13603  hashbc  13664  pfxval0  13879  sumz  14917  sumss  14919  fsumsplitsn  14938  sumsplit  14961  prod1  15136  prodss  15139  fprodsplitsn  15181  fprodle  15188  bitsmod  15623  sadadd2lem2  15637  sadcaddlem  15644  gcddvds  15690  gcdcl  15693  gcdneg  15708  dvdslcm  15776  lcmcl  15779  lcmneg  15781  lcmgcd  15785  lcmfcl  15806  dvdslcmf  15809  pcgcd  16048  pcmpt  16062  pcmpt2  16063  pcprod  16065  fldivp1  16067  prmreclem4  16089  vdwlem6  16156  ramub1lem1  16196  cidpropd  16814  rescabs  16937  lubval  17428  glbval  17441  joinval  17449  meetval  17463  acsexdimd  17627  gsumpropd2lem  17717  gsumval2  17724  mulgfval  17988  f1otrspeq  18311  pmtrfinv  18325  psgnunilem1  18357  gsumval3  18753  ablfac1c  18915  ablfac1eu  18917  mgpress  18945  psrbas  19851  resspsrbas  19888  mplmonmul  19937  mplcoe1  19938  mplcoe5  19941  opsrle  19948  opsrbaslem  19950  psrbaspropd  20091  mplbaspropd  20093  frlmsslsp  20627  mdetdiag  20897  mdetunilem7  20916  mdetunilem9  20918  maducoeval2  20938  madurid  20942  opnnei  21417  restbas  21455  hauspwdom  21798  ptcmplem5  22353  xrsmopn  23108  xrhmeo  23238  lebnum  23256  pcoass  23316  pcorevlem  23318  icombl  23853  ioombl  23854  mbfconstlem  23916  mbfima  23919  i1fd  23970  mbfi1fseqlem5  24008  itg2const2  24030  itg2seq  24031  itg2uba  24032  itg2splitlem  24037  itg2split  24038  itg2monolem1  24039  itg2gt0  24049  itg2cnlem1  24050  itg2cnlem2  24051  iblss  24093  iblss2  24094  itgss  24100  bddmulibl  24127  coemullem  24528  aaliou2b  24618  isppw2  25379  mule1  25412  ppip1le  25425  dchrelbas3  25501  dchrpt  25530  bposlem3  25549  bposlem5  25551  bposlem6  25552  lgslem4  25563  lgsneg  25584  lgsmod  25586  lgsdilem  25587  lgsdir  25595  lgsdi  25597  lgsne0  25598  lgsquad3  25650  dchrvmasum2if  25760  midexlem  26165  colperpex  26206  outpasch  26228  hlpasch  26229  lnopp2hpgb  26236  lmieu  26257  inaghl  26319  cgrg3col4  26327  pthdlem1  27239  nmcfnlbi  29525  elpreq  29984  disjdifprg  30020  disjun0  30040  f1ocnt  30214  xrge0npcan  30360  cyc3genpmlem  30436  cyc3conja  30442  archiabl  30470  orngsqr  30536  psgnfzto1stlem  30669  1smat1  30689  esumcst  30944  esumrnmpt2  30949  hasheuni  30966  esumcvg  30967  ddemeas  31117  omssubadd  31180  eulerpartlemgc  31242  eulerpartlemb  31248  plymulx  31440  signswmnd  31449  signstfvneq0  31464  pthhashvtx  31988  erdsze2lem1  32064  mrsubvrs  32383  trpredlem1  32681  unblimceq0lem  33460  unbdqndv2lem2  33464  knoppndvlem10  33475  wl-spae  34319  wl-cbvalnaed  34329  wl-nfeqfb  34333  unccur  34431  poimirlem15  34463  poimirlem22  34470  itg2addnclem  34499  itg2addnclem2  34500  iblmulc2nc  34513  ftc1anclem5  34527  ftc1anc  34531  dvasin  34534  areacirclem5  34542  exmid2  34934  3dim1  36159  3dim2  36160  3dim3  36161  3atlem3  36177  3atlem7  36181  lvolnle3at  36274  2lplnja  36311  paddasslem18  36529  lhpexle3lem  36703  4atex  36768  cdlemd5  36894  cdleme16  36977  cdleme20  37016  cdleme21j  37028  cdleme21  37029  cdleme32snaw  37127  cdleme32fvcl  37132  cdleme32le  37139  cdlemeg46gf  37225  cdleme48gfv  37229  cdleme50trn12  37244  cdlemg6  37315  cdlemg7N  37318  cdlemg38  37407  cdlemg46  37427  dibvalrel  37855  dihlss  37942  dihglblem5aN  37984  dihmeetbN  37995  dihmeetALTN  38019  dihatlat  38026  dihatexv  38030  dvh3dim2  38140  dvh3dim3N  38141  lclkrlem2h  38206  mapdh8d  38475  mapdh8g  38477  hdmap11lem2  38534  dffltz  38793  ttac  39143  pw2f1ocnv  39144  aomclem5  39168  isnumbasgrplem3  39215  iocmbl  39329  r1rankcld  40089  grur1cld  40090  grucollcld  40118  mnuprd  40134  radcnvrat  40209  bccbc  40240  binomcxp  40252  fnchoice  40850  fiiuncl  40891  eliin2f  40935  founiiun0  41016  axccdom  41052  axccd2  41061  fzisoeu  41133  fperiodmul  41137  upbdrech2  41141  fzdifsuc2  41143  uzfissfz  41160  supxrgere  41167  supxrgelem  41171  supxrge  41172  suplesup  41173  infrpge  41185  xrlexaddrp  41186  xralrple2  41188  infxr  41201  infleinflem1  41204  infleinflem2  41205  infleinf  41206  xralrple3  41208  fiminre2  41212  xrralrecnnge  41228  uzublem  41271  supxrmnf2  41274  infxrpnf  41288  infxrpnf2  41306  supminfxr  41307  supminfxr2  41312  ioondisj2  41334  iccdifprioo  41359  fmul01lt1lem1  41432  fmul01lt1lem2  41433  limciccioolb  41469  lptioo2  41479  lptioo1  41480  limcicciooub  41485  lptre2pt  41488  limcresiooub  41490  limcresioolb  41491  limcleqr  41492  climfveq  41517  climfveqf  41528  limsupubuzlem  41560  limsupubuz  41561  limsupmnfuzlem  41574  limsupre3uzlem  41583  climxrre  41598  limsup10exlem  41620  cnrefiisplem  41677  climxlim2lem  41693  dfxlim2v  41695  xlimliminflimsup  41710  coskpi2  41714  cosknegpi  41717  icccncfext  41737  cncfiooicclem1  41743  cncfiooicc  41744  cncfiooiccre  41745  dvbdfbdioolem2  41781  ioodvbdlimc1lem1  41783  ioodvbdlimc1lem2  41784  ioodvbdlimc2lem  41786  dvnxpaek  41794  dvnprodlem1  41798  dvnprodlem3  41800  volioc  41824  itgioocnicc  41829  iblcncfioo  41830  volico  41836  sublevolico  41837  ismbl3  41839  ovolsplit  41841  volioore  41843  voliooico  41845  voliccico  41852  stoweidlem14  41867  stoweidlem26  41879  stoweidlem28  41881  stoweidlem55  41908  stoweid  41916  stirlinglem5  41931  stirlinglem12  41938  dirkerper  41949  dirkertrigeqlem3  41953  dirkertrigeq  41954  dirkercncflem1  41956  dirkercncflem2  41957  dirkercncf  41960  fourierdlem10  41970  fourierdlem12  41972  fourierdlem24  41984  fourierdlem30  41990  fourierdlem31  41991  fourierdlem32  41992  fourierdlem33  41993  fourierdlem34  41994  fourierdlem35  41995  fourierdlem37  41997  fourierdlem40  42000  fourierdlem41  42001  fourierdlem42  42002  fourierdlem43  42003  fourierdlem44  42004  fourierdlem46  42005  fourierdlem48  42007  fourierdlem49  42008  fourierdlem51  42010  fourierdlem54  42013  fourierdlem62  42021  fourierdlem64  42023  fourierdlem65  42024  fourierdlem70  42029  fourierdlem71  42030  fourierdlem73  42032  fourierdlem74  42033  fourierdlem75  42034  fourierdlem78  42037  fourierdlem79  42038  fourierdlem80  42039  fourierdlem81  42040  fourierdlem82  42041  fourierdlem92  42051  fourierdlem93  42052  fourierdlem97  42056  fourierdlem101  42060  fourierdlem102  42061  fourierdlem103  42062  fourierdlem104  42063  fourierdlem109  42068  fourierdlem114  42073  sqwvfoura  42081  sqwvfourb  42082  fourierswlem  42083  fouriersw  42084  elaa2lem  42086  etransclem15  42102  etransclem19  42106  etransclem20  42107  etransclem22  42109  etransclem23  42110  etransclem24  42111  etransclem25  42112  etransclem27  42114  etransclem28  42115  etransclem35  42122  etransclem38  42125  qndenserrnbl  42148  ioorrnopn  42158  ioorrnopnxrlem  42159  ioorrnopnxr  42160  prsal  42171  salexct  42185  issalnnd  42196  sge0sn  42229  sge0tsms  42230  sge0cl  42231  sge0f1o  42232  sge0sup  42241  sge0less  42242  sge0pr  42244  sge0prle  42251  sge0le  42257  sge0split  42259  sge0splitmpt  42261  sge0iunmptlemfi  42263  sge0iunmpt  42268  sge0isum  42277  sge0xaddlem1  42283  sge0xadd  42285  sge0gtfsumgt  42293  nnfoctbdjlem  42305  iundjiun  42310  meadjun  42312  ismeannd  42317  voliunsge0lem  42322  meaiuninc3v  42334  caragenfiiuncl  42365  omeiunltfirp  42369  carageniuncl  42373  caragenunicl  42374  isomenndlem  42380  isomennd  42381  hoicvr  42398  ovnssle  42411  ovn0  42416  ovnsubadd  42422  hsphoidmvle2  42435  hoidmvval0b  42440  hoidmv1lelem1  42441  hoidmv1lelem2  42442  hoidmv1le  42444  hoidmvlelem2  42446  hoidmvlelem3  42447  hoidmvlelem5  42449  hoidmvle  42450  ovnhoilem1  42451  ovnhoi  42453  ovnlecvr2  42460  hspdifhsp  42466  hoidifhspdmvle  42470  hoiqssbl  42475  hspmbllem1  42476  hspmbllem2  42477  hspmbl  42479  hoimbl  42481  volico2  42491  ovolval2lem  42493  ovnsubadd2lem  42495  ovolval4lem1  42499  ovolval4lem2  42500  ovolval5lem1  42502  vonhoire  42522  iunhoiioo  42526  vonioo  42532  vonicc  42535  vonsn  42541  pimrecltpos  42555  incsmflem  42586  smfpimltxr  42592  smfconst  42594  decsmflem  42610  smfpimgtxr  42624  smfrec  42632  sharhght  42690  ichnfimlem3  43131  rrx2linest  44236