Theorem pm2.61dan 812

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  813  pm2.61dda  814  nfsb4t  2501  sbal2  2531  pm2.61danel  3047  ifeq1da  4506  ifeq2da  4507  ifeq12da  4508  ifclda  4510  ifeqda  4511  ifbothda  4513  2if2  4530  somin1  6084  xpcan  6128  fvmpti  6934  fvmptss  6947  funressn  7098  ovima0  7531  ordsuci  7747  suppssov1  8133  suppssov2  8134  oeoa  8518  oeoe  8520  omabs  8572  eceqoveq  8752  domdifsn  8980  pw2f1olem  9001  mapdom1  9062  imafiOLD  9207  marypha1lem  9324  supval2  9346  infdifsn  9554  ttrcltr  9613  ttrclselem1  9622  carden2b  9867  fidomtri  9893  dfac12lem2  10043  infunsdom1  10110  infunsdom  10111  itunisuc  10317  gchdomtri  10527  fiminre2  12077  xrmax2  13077  xrmin1  13078  ifle  13098  xnn0lem1lt  13145  xmulneg1  13170  xrsupsslem  13208  xrinfmsslem  13209  fzneuz  13510  seqf1olem1  13950  bccmpl  14218  bcval5  14227  bcpasc  14230  bccl  14231  hasheni  14257  hashfn  14284  hashdom  14288  hashdomi  14289  hashge1  14298  hashbc  14362  pfxval0  14586  sumz  15631  sumss  15633  fsumsplitsn  15653  sumsplit  15677  prod1  15853  prodss  15856  fprodsplitsn  15898  fprodle  15905  bitsmod  16349  sadadd2lem2  16363  sadcaddlem  16370  gcddvds  16416  gcdcl  16419  gcdneg  16435  dvdslcm  16511  lcmcl  16514  lcmneg  16516  lcmgcd  16520  lcmfcl  16541  dvdslcmf  16544  pcgcd  16792  pcmpt  16806  pcmpt2  16807  pcprod  16809  fldivp1  16811  prmreclem4  16833  vdwlem6  16900  ramub1lem1  16940  cidpropd  17618  rescabs  17742  lubval  18262  glbval  18275  joinval  18283  meetval  18297  acsexdimd  18467  gsumpropd2lem  18589  gsumval2  18596  mulgfval  18984  f1otrspeq  19361  pmtrfinv  19375  psgnunilem1  19407  gsumval3  19821  ablfac1c  19987  ablfac1eu  19989  mgpress  20070  orngsqr  20783  frlmsslsp  21735  psrbas  21872  resspsrbas  21912  mplmonmul  21972  mplcoe1  21973  mplcoe5  21976  opsrle  21983  opsrbaslem  21985  psrbaspropd  22148  mplbaspropd  22150  mdetdiag  22515  mdetunilem7  22534  mdetunilem9  22536  maducoeval2  22556  madurid  22560  opnnei  23036  restbas  23074  hauspwdom  23417  ptcmplem5  23972  xrsmopn  24729  xrhmeo  24872  lebnum  24891  pcoass  24952  pcorevlem  24954  icombl  25493  ioombl  25494  mbfconstlem  25556  mbfima  25559  i1fd  25610  mbfi1fseqlem5  25648  itg2const2  25670  itg2seq  25671  itg2uba  25672  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  iblss  25734  iblss2  25735  itgss  25741  bddmulibl  25768  coemullem  26183  aaliou2b  26277  isppw2  27053  mule1  27086  ppip1le  27099  dchrelbas3  27177  dchrpt  27206  bposlem3  27225  bposlem5  27227  bposlem6  27228  lgslem4  27239  lgsneg  27260  lgsmod  27262  lgsdilem  27263  lgsdir  27271  lgsdi  27273  lgsne0  27274  lgsquad3  27326  dchrvmasum2if  27436  maxs2  27706  mins1  27707  midexlem  28671  colperpex  28712  outpasch  28734  hlpasch  28735  lnopp2hpgb  28742  lmieu  28763  inaghl  28824  cgrg3col4  28832  pthdlem1  29746  nmcfnlbi  32034  elpreq  32510  prssad  32511  prssbd  32512  disjdifprg  32557  disjun0  32577  argcj  32736  f1ocnt  32787  xrge0npcan  33008  psgnfzto1stlem  33076  cyc3genpmlem  33127  cyc3conja  33133  archiabl  33174  erlval  33232  1arithufdlem3  33518  1arithufd  33520  esplyfval3  33612  resssra  33620  lbslelsp  33631  constrrecl  33803  constrinvcl  33807  constrsqrtcl  33813  1smat1  33838  esumcst  34097  esumrnmpt2  34102  hasheuni  34119  esumcvg  34120  ddemeas  34270  omssubadd  34334  eulerpartlemgc  34396  eulerpartlemb  34402  plymulx  34582  signswmnd  34591  fineqvnttrclselem1  35162  pthhashvtx  35193  erdsze2lem1  35268  mrsubvrs  35587  unblimceq0lem  36571  unbdqndv2lem2  36575  knoppndvlem10  36586  wl-spae  37586  wl-cbvalnaed  37597  wl-nfeqfb  37601  unccur  37664  poimirlem15  37696  poimirlem22  37703  itg2addnclem  37732  itg2addnclem2  37733  iblmulc2nc  37746  ftc1anclem5  37758  ftc1anc  37762  dvasin  37765  areacirclem5  37773  exmid2  38160  3dim1  39587  3dim2  39588  3dim3  39589  3atlem3  39605  3atlem7  39609  lvolnle3at  39702  2lplnja  39739  paddasslem18  39957  lhpexle3lem  40131  4atex  40196  cdlemd5  40322  cdleme16  40405  cdleme20  40444  cdleme21j  40456  cdleme21  40457  cdleme32snaw  40555  cdleme32fvcl  40560  cdleme32le  40567  cdlemeg46gf  40653  cdleme48gfv  40657  cdleme50trn12  40672  cdlemg6  40743  cdlemg7N  40746  cdlemg38  40835  cdlemg46  40855  dibvalrel  41283  dihlss  41370  dihglblem5aN  41412  dihmeetbN  41423  dihmeetALTN  41447  dihatlat  41454  dihatexv  41458  dvh3dim2  41568  dvh3dim3N  41569  lclkrlem2h  41634  mapdh8d  41903  mapdh8g  41905  hdmap11lem2  41962  lcmineqlem23  42165  aks4d1p3  42192  aks4d1p5  42194  aks4d1p7d1  42196  posbezout  42214  aks6d1c2p2  42233  aks6d1c4  42238  aks6d1c5lem1  42250  aks6d1c6lem3  42286  aks6d1c6lem4  42287  bcled  42292  bcle2d  42293  aks6d1c7  42298  grpods  42308  unitscyglem2  42310  unitscyglem4  42312  aks5lem8  42315  dffltz  42753  ttac  43154  pw2f1ocnv  43155  aomclem5  43176  isnumbasgrplem3  43223  iocmbl  43331  oe0suclim  43395  tfsconcatfv  43459  safesnsupfidom1o  43535  safesnsupfilb  43536  r1rankcld  44349  grur1cld  44350  grucollcld  44378  mnuprd  44394  radcnvrat  44432  bccbc  44463  binomcxp  44475  fnchoice  45151  fiiuncl  45187  eliin2f  45226  founiiun0  45312  axccdom  45344  axccd2  45352  fzisoeu  45426  fperiodmul  45430  upbdrech2  45434  fzdifsuc2  45436  uzfissfz  45450  supxrgere  45457  supxrgelem  45461  supxrge  45462  suplesup  45463  infrpge  45475  xrlexaddrp  45476  xralrple2  45478  infxr  45490  infleinflem1  45493  infleinflem2  45494  infleinf  45495  xralrple3  45497  xrralrecnnge  45513  uzublem  45553  supxrmnf2  45556  infxrpnf  45569  infxrpnf2  45586  supminfxr  45587  supminfxr2  45592  pimxrneun  45611  rexanuz2nf  45615  ioondisj2  45618  iccdifprioo  45641  fmul01lt1lem1  45709  fmul01lt1lem2  45710  limciccioolb  45746  lptioo2  45756  lptioo1  45757  limcicciooub  45760  lptre2pt  45763  limcresiooub  45765  limcresioolb  45766  limcleqr  45767  climfveq  45792  climfveqf  45803  limsupubuzlem  45835  limsupubuz  45836  limsupmnfuzlem  45849  limsupre3uzlem  45858  climxrre  45873  limsup10exlem  45895  cnrefiisplem  45952  climxlim2lem  45968  dfxlim2v  45970  xlimliminflimsup  45985  coskpi2  45989  cosknegpi  45992  icccncfext  46010  cncfiooicclem1  46016  cncfiooicc  46017  cncfiooiccre  46018  dvbdfbdioolem2  46052  ioodvbdlimc1lem1  46054  ioodvbdlimc1lem2  46055  ioodvbdlimc2lem  46057  dvnxpaek  46065  dvnprodlem1  46069  dvnprodlem3  46071  volioc  46095  itgioocnicc  46100  iblcncfioo  46101  volico  46106  sublevolico  46107  ismbl3  46109  ovolsplit  46111  volioore  46113  voliooico  46115  voliccico  46122  stoweidlem14  46137  stoweidlem26  46149  stoweidlem28  46151  stoweidlem55  46178  stoweid  46186  stirlinglem5  46201  stirlinglem12  46208  dirkerper  46219  dirkertrigeqlem3  46223  dirkertrigeq  46224  dirkercncflem1  46226  dirkercncflem2  46227  dirkercncf  46230  fourierdlem10  46240  fourierdlem12  46242  fourierdlem24  46254  fourierdlem30  46260  fourierdlem31  46261  fourierdlem32  46262  fourierdlem33  46263  fourierdlem34  46264  fourierdlem35  46265  fourierdlem37  46267  fourierdlem40  46270  fourierdlem41  46271  fourierdlem42  46272  fourierdlem43  46273  fourierdlem44  46274  fourierdlem46  46275  fourierdlem48  46277  fourierdlem49  46278  fourierdlem51  46280  fourierdlem54  46283  fourierdlem62  46291  fourierdlem64  46293  fourierdlem65  46294  fourierdlem70  46299  fourierdlem71  46300  fourierdlem73  46302  fourierdlem74  46303  fourierdlem75  46304  fourierdlem78  46307  fourierdlem79  46308  fourierdlem80  46309  fourierdlem81  46310  fourierdlem82  46311  fourierdlem92  46321  fourierdlem93  46322  fourierdlem97  46326  fourierdlem101  46330  fourierdlem102  46331  fourierdlem103  46332  fourierdlem104  46333  fourierdlem109  46338  fourierdlem114  46343  sqwvfoura  46351  sqwvfourb  46352  fourierswlem  46353  fouriersw  46354  elaa2lem  46356  etransclem15  46372  etransclem19  46376  etransclem20  46377  etransclem22  46379  etransclem23  46380  etransclem24  46381  etransclem25  46382  etransclem27  46384  etransclem28  46385  etransclem35  46392  etransclem38  46395  qndenserrnbl  46418  ioorrnopn  46428  ioorrnopnxrlem  46429  ioorrnopnxr  46430  prsal  46441  salexct  46457  issalnnd  46468  sge0sn  46502  sge0tsms  46503  sge0cl  46504  sge0f1o  46505  sge0sup  46514  sge0less  46515  sge0pr  46517  sge0prle  46524  sge0le  46530  sge0split  46532  sge0splitmpt  46534  sge0iunmptlemfi  46536  sge0iunmpt  46541  sge0isum  46550  sge0xaddlem1  46556  sge0xadd  46558  sge0gtfsumgt  46566  nnfoctbdjlem  46578  iundjiun  46583  meadjun  46585  ismeannd  46590  voliunsge0lem  46595  meaiuninc3v  46607  caragenfiiuncl  46638  omeiunltfirp  46642  carageniuncl  46646  caragenunicl  46647  isomenndlem  46653  isomennd  46654  hoicvr  46671  ovnssle  46684  ovn0  46689  ovnsubadd  46695  hsphoidmvle2  46708  hoidmvval0b  46713  hoidmv1lelem1  46714  hoidmv1lelem2  46715  hoidmv1le  46717  hoidmvlelem2  46719  hoidmvlelem3  46720  hoidmvlelem5  46722  hoidmvle  46723  ovnhoilem1  46724  ovnhoi  46726  ovnlecvr2  46733  hspdifhsp  46739  hoidifhspdmvle  46743  hoiqssbl  46748  hspmbllem1  46749  hspmbllem2  46750  hspmbl  46752  hoimbl  46754  volico2  46764  ovolval2lem  46766  ovnsubadd2lem  46768  ovolval4lem1  46772  ovolval4lem2  46773  ovolval5lem1  46775  vonhoire  46795  iunhoiioo  46799  vonioo  46805  vonicc  46808  vonsn  46814  pimrecltpos  46831  incsmflem  46864  smfpimltxr  46870  smfconst  46872  decsmflem  46889  smfpimgtxr  46903  smfrec  46912  smfpimne2  46963  sharhght  46988  rrx2linest  48868  mofsn2  48970  ipolub00  49118  resccat  49200  initopropdlemlem  49365  prcof1  49514