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  2497  sbal2  2527  pm2.61danel  3043  ifeq1da  4520  ifeq2da  4521  ifeq12da  4522  ifclda  4524  ifeqda  4525  ifbothda  4527  2if2  4544  somin1  6106  xpcan  6149  fvmpti  6967  fvmptss  6980  funressn  7131  ovima0  7568  ordsuci  7784  suppssov1  8176  suppssov2  8177  oeoa  8561  oeoe  8563  omabs  8615  eceqoveq  8795  domdifsn  9024  pw2f1olem  9045  mapdom1  9106  imafiOLD  9265  marypha1lem  9384  supval2  9406  infdifsn  9610  ttrcltr  9669  ttrclselem1  9678  carden2b  9920  fidomtri  9946  dfac12lem2  10098  infunsdom1  10165  infunsdom  10166  itunisuc  10372  gchdomtri  10582  fiminre2  12131  xrmax2  13136  xrmin1  13137  ifle  13157  xnn0lem1lt  13204  xmulneg1  13229  xrsupsslem  13267  xrinfmsslem  13268  fzneuz  13569  seqf1olem1  14006  bccmpl  14274  bcval5  14283  bcpasc  14286  bccl  14287  hasheni  14313  hashfn  14340  hashdom  14344  hashdomi  14345  hashge1  14354  hashbc  14418  pfxval0  14641  sumz  15688  sumss  15690  fsumsplitsn  15710  sumsplit  15734  prod1  15910  prodss  15913  fprodsplitsn  15955  fprodle  15962  bitsmod  16406  sadadd2lem2  16420  sadcaddlem  16427  gcddvds  16473  gcdcl  16476  gcdneg  16492  dvdslcm  16568  lcmcl  16571  lcmneg  16573  lcmgcd  16577  lcmfcl  16598  dvdslcmf  16601  pcgcd  16849  pcmpt  16863  pcmpt2  16864  pcprod  16866  fldivp1  16868  prmreclem4  16890  vdwlem6  16957  ramub1lem1  16997  cidpropd  17671  rescabs  17795  lubval  18315  glbval  18328  joinval  18336  meetval  18350  acsexdimd  18518  gsumpropd2lem  18606  gsumval2  18613  mulgfval  19001  f1otrspeq  19377  pmtrfinv  19391  psgnunilem1  19423  gsumval3  19837  ablfac1c  20003  ablfac1eu  20005  mgpress  20059  frlmsslsp  21705  psrbas  21842  resspsrbas  21883  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  opsrle  21954  opsrbaslem  21956  psrbaspropd  22119  mplbaspropd  22121  mdetdiag  22486  mdetunilem7  22505  mdetunilem9  22507  maducoeval2  22527  madurid  22531  opnnei  23007  restbas  23045  hauspwdom  23388  ptcmplem5  23943  xrsmopn  24701  xrhmeo  24844  lebnum  24863  pcoass  24924  pcorevlem  24926  icombl  25465  ioombl  25466  mbfconstlem  25528  mbfima  25531  i1fd  25582  mbfi1fseqlem5  25620  itg2const2  25642  itg2seq  25643  itg2uba  25644  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  iblss2  25707  itgss  25713  bddmulibl  25740  coemullem  26155  aaliou2b  26249  isppw2  27025  mule1  27058  ppip1le  27071  dchrelbas3  27149  dchrpt  27178  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgslem4  27211  lgsneg  27232  lgsmod  27234  lgsdilem  27235  lgsdir  27243  lgsdi  27245  lgsne0  27246  lgsquad3  27298  dchrvmasum2if  27408  maxs2  27678  mins1  27679  midexlem  28619  colperpex  28660  outpasch  28682  hlpasch  28683  lnopp2hpgb  28690  lmieu  28711  inaghl  28772  cgrg3col4  28780  pthdlem1  29696  nmcfnlbi  31981  elpreq  32457  prssad  32458  prssbd  32459  disjdifprg  32504  disjun0  32524  argcj  32672  f1ocnt  32725  xrge0npcan  32961  psgnfzto1stlem  33057  cyc3genpmlem  33108  cyc3conja  33114  archiabl  33152  erlval  33209  orngsqr  33282  1arithufdlem3  33517  1arithufd  33519  resssra  33583  lbslelsp  33593  constrrecl  33759  constrinvcl  33763  constrsqrtcl  33769  1smat1  33794  esumcst  34053  esumrnmpt2  34058  hasheuni  34075  esumcvg  34076  ddemeas  34226  omssubadd  34291  eulerpartlemgc  34353  eulerpartlemb  34359  plymulx  34539  signswmnd  34548  pthhashvtx  35115  erdsze2lem1  35190  mrsubvrs  35509  unblimceq0lem  36494  unbdqndv2lem2  36498  knoppndvlem10  36509  wl-spae  37509  wl-cbvalnaed  37520  wl-nfeqfb  37524  unccur  37597  poimirlem15  37629  poimirlem22  37636  itg2addnclem  37665  itg2addnclem2  37666  iblmulc2nc  37679  ftc1anclem5  37691  ftc1anc  37695  dvasin  37698  areacirclem5  37706  exmid2  38093  3dim1  39461  3dim2  39462  3dim3  39463  3atlem3  39479  3atlem7  39483  lvolnle3at  39576  2lplnja  39613  paddasslem18  39831  lhpexle3lem  40005  4atex  40070  cdlemd5  40196  cdleme16  40279  cdleme20  40318  cdleme21j  40330  cdleme21  40331  cdleme32snaw  40429  cdleme32fvcl  40434  cdleme32le  40441  cdlemeg46gf  40527  cdleme48gfv  40531  cdleme50trn12  40546  cdlemg6  40617  cdlemg7N  40620  cdlemg38  40709  cdlemg46  40729  dibvalrel  41157  dihlss  41244  dihglblem5aN  41286  dihmeetbN  41297  dihmeetALTN  41321  dihatlat  41328  dihatexv  41332  dvh3dim2  41442  dvh3dim3N  41443  lclkrlem2h  41508  mapdh8d  41777  mapdh8g  41779  hdmap11lem2  41836  lcmineqlem23  42039  aks4d1p3  42066  aks4d1p5  42068  aks4d1p7d1  42070  posbezout  42088  aks6d1c2p2  42107  aks6d1c4  42112  aks6d1c5lem1  42124  aks6d1c6lem3  42160  aks6d1c6lem4  42161  bcled  42166  bcle2d  42167  aks6d1c7  42172  grpods  42182  unitscyglem2  42184  unitscyglem4  42186  aks5lem8  42189  dffltz  42622  ttac  43025  pw2f1ocnv  43026  aomclem5  43047  isnumbasgrplem3  43094  iocmbl  43202  oe0suclim  43266  tfsconcatfv  43330  safesnsupfidom1o  43406  safesnsupfilb  43407  r1rankcld  44220  grur1cld  44221  grucollcld  44249  mnuprd  44265  radcnvrat  44303  bccbc  44334  binomcxp  44346  fnchoice  45023  fiiuncl  45059  eliin2f  45098  founiiun0  45184  axccdom  45216  axccd2  45224  fzisoeu  45298  fperiodmul  45302  upbdrech2  45306  fzdifsuc2  45308  uzfissfz  45322  supxrgere  45329  supxrgelem  45333  supxrge  45334  suplesup  45335  infrpge  45347  xrlexaddrp  45348  xralrple2  45350  infxr  45363  infleinflem1  45366  infleinflem2  45367  infleinf  45368  xralrple3  45370  xrralrecnnge  45386  uzublem  45426  supxrmnf2  45429  infxrpnf  45442  infxrpnf2  45459  supminfxr  45460  supminfxr2  45465  pimxrneun  45484  rexanuz2nf  45488  ioondisj2  45491  iccdifprioo  45514  fmul01lt1lem1  45582  fmul01lt1lem2  45583  limciccioolb  45619  lptioo2  45629  lptioo1  45630  limcicciooub  45635  lptre2pt  45638  limcresiooub  45640  limcresioolb  45641  limcleqr  45642  climfveq  45667  climfveqf  45678  limsupubuzlem  45710  limsupubuz  45711  limsupmnfuzlem  45724  limsupre3uzlem  45733  climxrre  45748  limsup10exlem  45770  cnrefiisplem  45827  climxlim2lem  45843  dfxlim2v  45845  xlimliminflimsup  45860  coskpi2  45864  cosknegpi  45867  icccncfext  45885  cncfiooicclem1  45891  cncfiooicc  45892  cncfiooiccre  45893  dvbdfbdioolem2  45927  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnprodlem1  45944  dvnprodlem3  45946  volioc  45970  itgioocnicc  45975  iblcncfioo  45976  volico  45981  sublevolico  45982  ismbl3  45984  ovolsplit  45986  volioore  45988  voliooico  45990  voliccico  45997  stoweidlem14  46012  stoweidlem26  46024  stoweidlem28  46026  stoweidlem55  46053  stoweid  46061  stirlinglem5  46076  stirlinglem12  46083  dirkerper  46094  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncf  46105  fourierdlem10  46115  fourierdlem12  46117  fourierdlem24  46129  fourierdlem30  46135  fourierdlem31  46136  fourierdlem32  46137  fourierdlem33  46138  fourierdlem34  46139  fourierdlem35  46140  fourierdlem37  46142  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem43  46148  fourierdlem44  46149  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem54  46158  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem80  46184  fourierdlem81  46185  fourierdlem82  46186  fourierdlem92  46196  fourierdlem93  46197  fourierdlem97  46201  fourierdlem101  46205  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem109  46213  fourierdlem114  46218  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem15  46247  etransclem19  46251  etransclem20  46252  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem27  46259  etransclem28  46260  etransclem35  46267  etransclem38  46270  qndenserrnbl  46293  ioorrnopn  46303  ioorrnopnxrlem  46304  ioorrnopnxr  46305  prsal  46316  salexct  46332  issalnnd  46343  sge0sn  46377  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0sup  46389  sge0less  46390  sge0pr  46392  sge0prle  46399  sge0le  46405  sge0split  46407  sge0splitmpt  46409  sge0iunmptlemfi  46411  sge0iunmpt  46416  sge0isum  46425  sge0xaddlem1  46431  sge0xadd  46433  sge0gtfsumgt  46441  nnfoctbdjlem  46453  iundjiun  46458  meadjun  46460  ismeannd  46465  voliunsge0lem  46470  meaiuninc3v  46482  caragenfiiuncl  46513  omeiunltfirp  46517  carageniuncl  46521  caragenunicl  46522  isomenndlem  46528  isomennd  46529  hoicvr  46546  ovnssle  46559  ovn0  46564  ovnsubadd  46570  hsphoidmvle2  46583  hoidmvval0b  46588  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem5  46597  hoidmvle  46598  ovnhoilem1  46599  ovnhoi  46601  ovnlecvr2  46608  hspdifhsp  46614  hoidifhspdmvle  46618  hoiqssbl  46623  hspmbllem1  46624  hspmbllem2  46625  hspmbl  46627  hoimbl  46629  volico2  46639  ovolval2lem  46641  ovnsubadd2lem  46643  ovolval4lem1  46647  ovolval4lem2  46648  ovolval5lem1  46650  vonhoire  46670  iunhoiioo  46674  vonioo  46680  vonicc  46683  vonsn  46689  pimrecltpos  46706  incsmflem  46739  smfpimltxr  46745  smfconst  46747  decsmflem  46764  smfpimgtxr  46778  smfrec  46787  smfpimne2  46838  sharhght  46863  rrx2linest  48731  mofsn2  48833  ipolub00  48981  resccat  49063  initopropdlemlem  49228  prcof1  49377