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  4510  ifeq2da  4511  ifeq12da  4512  ifclda  4514  ifeqda  4515  ifbothda  4517  2if2  4534  somin1  6086  xpcan  6129  fvmpti  6933  fvmptss  6946  funressn  7097  ovima0  7532  ordsuci  7748  suppssov1  8137  suppssov2  8138  oeoa  8522  oeoe  8524  omabs  8576  eceqoveq  8756  domdifsn  8984  pw2f1olem  9005  mapdom1  9066  imafiOLD  9223  marypha1lem  9342  supval2  9364  infdifsn  9572  ttrcltr  9631  ttrclselem1  9640  carden2b  9882  fidomtri  9908  dfac12lem2  10058  infunsdom1  10125  infunsdom  10126  itunisuc  10332  gchdomtri  10542  fiminre2  12091  xrmax2  13096  xrmin1  13097  ifle  13117  xnn0lem1lt  13164  xmulneg1  13189  xrsupsslem  13227  xrinfmsslem  13228  fzneuz  13529  seqf1olem1  13966  bccmpl  14234  bcval5  14243  bcpasc  14246  bccl  14247  hasheni  14273  hashfn  14300  hashdom  14304  hashdomi  14305  hashge1  14314  hashbc  14378  pfxval0  14601  sumz  15647  sumss  15649  fsumsplitsn  15669  sumsplit  15693  prod1  15869  prodss  15872  fprodsplitsn  15914  fprodle  15921  bitsmod  16365  sadadd2lem2  16379  sadcaddlem  16386  gcddvds  16432  gcdcl  16435  gcdneg  16451  dvdslcm  16527  lcmcl  16530  lcmneg  16532  lcmgcd  16536  lcmfcl  16557  dvdslcmf  16560  pcgcd  16808  pcmpt  16822  pcmpt2  16823  pcprod  16825  fldivp1  16827  prmreclem4  16849  vdwlem6  16916  ramub1lem1  16956  cidpropd  17634  rescabs  17758  lubval  18278  glbval  18291  joinval  18299  meetval  18313  acsexdimd  18483  gsumpropd2lem  18571  gsumval2  18578  mulgfval  18966  f1otrspeq  19344  pmtrfinv  19358  psgnunilem1  19390  gsumval3  19804  ablfac1c  19970  ablfac1eu  19972  mgpress  20053  orngsqr  20769  frlmsslsp  21721  psrbas  21858  resspsrbas  21899  mplmonmul  21959  mplcoe1  21960  mplcoe5  21963  opsrle  21970  opsrbaslem  21972  psrbaspropd  22135  mplbaspropd  22137  mdetdiag  22502  mdetunilem7  22521  mdetunilem9  22523  maducoeval2  22543  madurid  22547  opnnei  23023  restbas  23061  hauspwdom  23404  ptcmplem5  23959  xrsmopn  24717  xrhmeo  24860  lebnum  24879  pcoass  24940  pcorevlem  24942  icombl  25481  ioombl  25482  mbfconstlem  25544  mbfima  25547  i1fd  25598  mbfi1fseqlem5  25636  itg2const2  25658  itg2seq  25659  itg2uba  25660  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25722  iblss2  25723  itgss  25729  bddmulibl  25756  coemullem  26171  aaliou2b  26265  isppw2  27041  mule1  27074  ppip1le  27087  dchrelbas3  27165  dchrpt  27194  bposlem3  27213  bposlem5  27215  bposlem6  27216  lgslem4  27227  lgsneg  27248  lgsmod  27250  lgsdilem  27251  lgsdir  27259  lgsdi  27261  lgsne0  27262  lgsquad3  27314  dchrvmasum2if  27424  maxs2  27694  mins1  27695  midexlem  28655  colperpex  28696  outpasch  28718  hlpasch  28719  lnopp2hpgb  28726  lmieu  28747  inaghl  28808  cgrg3col4  28816  pthdlem1  29729  nmcfnlbi  32014  elpreq  32490  prssad  32491  prssbd  32492  disjdifprg  32537  disjun0  32557  argcj  32705  f1ocnt  32758  xrge0npcan  32987  psgnfzto1stlem  33055  cyc3genpmlem  33106  cyc3conja  33112  archiabl  33150  erlval  33208  1arithufdlem3  33493  1arithufd  33495  resssra  33559  lbslelsp  33569  constrrecl  33735  constrinvcl  33739  constrsqrtcl  33745  1smat1  33770  esumcst  34029  esumrnmpt2  34034  hasheuni  34051  esumcvg  34052  ddemeas  34202  omssubadd  34267  eulerpartlemgc  34329  eulerpartlemb  34335  plymulx  34515  signswmnd  34524  pthhashvtx  35100  erdsze2lem1  35175  mrsubvrs  35494  unblimceq0lem  36479  unbdqndv2lem2  36483  knoppndvlem10  36494  wl-spae  37494  wl-cbvalnaed  37505  wl-nfeqfb  37509  unccur  37582  poimirlem15  37614  poimirlem22  37621  itg2addnclem  37650  itg2addnclem2  37651  iblmulc2nc  37664  ftc1anclem5  37676  ftc1anc  37680  dvasin  37683  areacirclem5  37691  exmid2  38078  3dim1  39446  3dim2  39447  3dim3  39448  3atlem3  39464  3atlem7  39468  lvolnle3at  39561  2lplnja  39598  paddasslem18  39816  lhpexle3lem  39990  4atex  40055  cdlemd5  40181  cdleme16  40264  cdleme20  40303  cdleme21j  40315  cdleme21  40316  cdleme32snaw  40414  cdleme32fvcl  40419  cdleme32le  40426  cdlemeg46gf  40512  cdleme48gfv  40516  cdleme50trn12  40531  cdlemg6  40602  cdlemg7N  40605  cdlemg38  40694  cdlemg46  40714  dibvalrel  41142  dihlss  41229  dihglblem5aN  41271  dihmeetbN  41282  dihmeetALTN  41306  dihatlat  41313  dihatexv  41317  dvh3dim2  41427  dvh3dim3N  41428  lclkrlem2h  41493  mapdh8d  41762  mapdh8g  41764  hdmap11lem2  41821  lcmineqlem23  42024  aks4d1p3  42051  aks4d1p5  42053  aks4d1p7d1  42055  posbezout  42073  aks6d1c2p2  42092  aks6d1c4  42097  aks6d1c5lem1  42109  aks6d1c6lem3  42145  aks6d1c6lem4  42146  bcled  42151  bcle2d  42152  aks6d1c7  42157  grpods  42167  unitscyglem2  42169  unitscyglem4  42171  aks5lem8  42174  dffltz  42607  ttac  43009  pw2f1ocnv  43010  aomclem5  43031  isnumbasgrplem3  43078  iocmbl  43186  oe0suclim  43250  tfsconcatfv  43314  safesnsupfidom1o  43390  safesnsupfilb  43391  r1rankcld  44204  grur1cld  44205  grucollcld  44233  mnuprd  44249  radcnvrat  44287  bccbc  44318  binomcxp  44330  fnchoice  45007  fiiuncl  45043  eliin2f  45082  founiiun0  45168  axccdom  45200  axccd2  45208  fzisoeu  45282  fperiodmul  45286  upbdrech2  45290  fzdifsuc2  45292  uzfissfz  45306  supxrgere  45313  supxrgelem  45317  supxrge  45318  suplesup  45319  infrpge  45331  xrlexaddrp  45332  xralrple2  45334  infxr  45347  infleinflem1  45350  infleinflem2  45351  infleinf  45352  xralrple3  45354  xrralrecnnge  45370  uzublem  45410  supxrmnf2  45413  infxrpnf  45426  infxrpnf2  45443  supminfxr  45444  supminfxr2  45449  pimxrneun  45468  rexanuz2nf  45472  ioondisj2  45475  iccdifprioo  45498  fmul01lt1lem1  45566  fmul01lt1lem2  45567  limciccioolb  45603  lptioo2  45613  lptioo1  45614  limcicciooub  45619  lptre2pt  45622  limcresiooub  45624  limcresioolb  45625  limcleqr  45626  climfveq  45651  climfveqf  45662  limsupubuzlem  45694  limsupubuz  45695  limsupmnfuzlem  45708  limsupre3uzlem  45717  climxrre  45732  limsup10exlem  45754  cnrefiisplem  45811  climxlim2lem  45827  dfxlim2v  45829  xlimliminflimsup  45844  coskpi2  45848  cosknegpi  45851  icccncfext  45869  cncfiooicclem1  45875  cncfiooicc  45876  cncfiooiccre  45877  dvbdfbdioolem2  45911  ioodvbdlimc1lem1  45913  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvnxpaek  45924  dvnprodlem1  45928  dvnprodlem3  45930  volioc  45954  itgioocnicc  45959  iblcncfioo  45960  volico  45965  sublevolico  45966  ismbl3  45968  ovolsplit  45970  volioore  45972  voliooico  45974  voliccico  45981  stoweidlem14  45996  stoweidlem26  46008  stoweidlem28  46010  stoweidlem55  46037  stoweid  46045  stirlinglem5  46060  stirlinglem12  46067  dirkerper  46078  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem1  46085  dirkercncflem2  46086  dirkercncf  46089  fourierdlem10  46099  fourierdlem12  46101  fourierdlem24  46113  fourierdlem30  46119  fourierdlem31  46120  fourierdlem32  46121  fourierdlem33  46122  fourierdlem34  46123  fourierdlem35  46124  fourierdlem37  46126  fourierdlem40  46129  fourierdlem41  46130  fourierdlem42  46131  fourierdlem43  46132  fourierdlem44  46133  fourierdlem46  46134  fourierdlem48  46136  fourierdlem49  46137  fourierdlem51  46139  fourierdlem54  46142  fourierdlem62  46150  fourierdlem64  46152  fourierdlem65  46153  fourierdlem70  46158  fourierdlem71  46159  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem78  46166  fourierdlem79  46167  fourierdlem80  46168  fourierdlem81  46169  fourierdlem82  46170  fourierdlem92  46180  fourierdlem93  46181  fourierdlem97  46185  fourierdlem101  46189  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem109  46197  fourierdlem114  46202  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  elaa2lem  46215  etransclem15  46231  etransclem19  46235  etransclem20  46236  etransclem22  46238  etransclem23  46239  etransclem24  46240  etransclem25  46241  etransclem27  46243  etransclem28  46244  etransclem35  46251  etransclem38  46254  qndenserrnbl  46277  ioorrnopn  46287  ioorrnopnxrlem  46288  ioorrnopnxr  46289  prsal  46300  salexct  46316  issalnnd  46327  sge0sn  46361  sge0tsms  46362  sge0cl  46363  sge0f1o  46364  sge0sup  46373  sge0less  46374  sge0pr  46376  sge0prle  46383  sge0le  46389  sge0split  46391  sge0splitmpt  46393  sge0iunmptlemfi  46395  sge0iunmpt  46400  sge0isum  46409  sge0xaddlem1  46415  sge0xadd  46417  sge0gtfsumgt  46425  nnfoctbdjlem  46437  iundjiun  46442  meadjun  46444  ismeannd  46449  voliunsge0lem  46454  meaiuninc3v  46466  caragenfiiuncl  46497  omeiunltfirp  46501  carageniuncl  46505  caragenunicl  46506  isomenndlem  46512  isomennd  46513  hoicvr  46530  ovnssle  46543  ovn0  46548  ovnsubadd  46554  hsphoidmvle2  46567  hoidmvval0b  46572  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmv1le  46576  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem5  46581  hoidmvle  46582  ovnhoilem1  46583  ovnhoi  46585  ovnlecvr2  46592  hspdifhsp  46598  hoidifhspdmvle  46602  hoiqssbl  46607  hspmbllem1  46608  hspmbllem2  46609  hspmbl  46611  hoimbl  46613  volico2  46623  ovolval2lem  46625  ovnsubadd2lem  46627  ovolval4lem1  46631  ovolval4lem2  46632  ovolval5lem1  46634  vonhoire  46654  iunhoiioo  46658  vonioo  46664  vonicc  46667  vonsn  46673  pimrecltpos  46690  incsmflem  46723  smfpimltxr  46729  smfconst  46731  decsmflem  46748  smfpimgtxr  46762  smfrec  46771  smfpimne2  46822  sharhght  46847  rrx2linest  48728  mofsn2  48830  ipolub00  48978  resccat  49060  initopropdlemlem  49225  prcof1  49374