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  2503  sbal2  2533  pm2.61danel  3050  ifeq1da  4532  ifeq2da  4533  ifeq12da  4534  ifclda  4536  ifeqda  4537  ifbothda  4539  2if2  4556  somin1  6122  xpcan  6165  fvmpti  6984  fvmptss  6997  funressn  7148  ovima0  7584  ordsuci  7800  suppssov1  8194  suppssov2  8195  oeoa  8607  oeoe  8609  omabs  8661  eceqoveq  8834  domdifsn  9066  pw2f1olem  9088  mapdom1  9154  imafiOLD  9324  marypha1lem  9443  supval2  9465  infdifsn  9669  ttrcltr  9728  ttrclselem1  9737  carden2b  9979  fidomtri  10005  dfac12lem2  10157  infunsdom1  10224  infunsdom  10225  itunisuc  10431  gchdomtri  10641  fiminre2  12188  xrmax2  13190  xrmin1  13191  ifle  13211  xnn0lem1lt  13258  xmulneg1  13283  xrsupsslem  13321  xrinfmsslem  13322  fzneuz  13623  seqf1olem1  14057  bccmpl  14325  bcval5  14334  bcpasc  14337  bccl  14338  hasheni  14364  hashfn  14391  hashdom  14395  hashdomi  14396  hashge1  14405  hashbc  14469  pfxval0  14692  sumz  15736  sumss  15738  fsumsplitsn  15758  sumsplit  15782  prod1  15958  prodss  15961  fprodsplitsn  16003  fprodle  16010  bitsmod  16453  sadadd2lem2  16467  sadcaddlem  16474  gcddvds  16520  gcdcl  16523  gcdneg  16539  dvdslcm  16615  lcmcl  16618  lcmneg  16620  lcmgcd  16624  lcmfcl  16645  dvdslcmf  16648  pcgcd  16896  pcmpt  16910  pcmpt2  16911  pcprod  16913  fldivp1  16915  prmreclem4  16937  vdwlem6  17004  ramub1lem1  17044  cidpropd  17720  rescabs  17844  lubval  18364  glbval  18377  joinval  18385  meetval  18399  acsexdimd  18567  gsumpropd2lem  18655  gsumval2  18662  mulgfval  19050  f1otrspeq  19426  pmtrfinv  19440  psgnunilem1  19472  gsumval3  19886  ablfac1c  20052  ablfac1eu  20054  mgpress  20108  frlmsslsp  21754  psrbas  21891  resspsrbas  21932  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  opsrle  22003  opsrbaslem  22005  psrbaspropd  22168  mplbaspropd  22170  mdetdiag  22535  mdetunilem7  22554  mdetunilem9  22556  maducoeval2  22576  madurid  22580  opnnei  23056  restbas  23094  hauspwdom  23437  ptcmplem5  23992  xrsmopn  24750  xrhmeo  24893  lebnum  24912  pcoass  24973  pcorevlem  24975  icombl  25515  ioombl  25516  mbfconstlem  25578  mbfima  25581  i1fd  25632  mbfi1fseqlem5  25670  itg2const2  25692  itg2seq  25693  itg2uba  25694  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  iblss  25756  iblss2  25757  itgss  25763  bddmulibl  25790  coemullem  26205  aaliou2b  26299  isppw2  27075  mule1  27108  ppip1le  27121  dchrelbas3  27199  dchrpt  27228  bposlem3  27247  bposlem5  27249  bposlem6  27250  lgslem4  27261  lgsneg  27282  lgsmod  27284  lgsdilem  27285  lgsdir  27293  lgsdi  27295  lgsne0  27296  lgsquad3  27348  dchrvmasum2if  27458  maxs2  27728  mins1  27729  midexlem  28617  colperpex  28658  outpasch  28680  hlpasch  28681  lnopp2hpgb  28688  lmieu  28709  inaghl  28770  cgrg3col4  28778  pthdlem1  29694  nmcfnlbi  31979  elpreq  32455  prssad  32456  prssbd  32457  disjdifprg  32502  disjun0  32522  argcj  32672  f1ocnt  32725  xrge0npcan  32961  psgnfzto1stlem  33057  cyc3genpmlem  33108  cyc3conja  33114  archiabl  33142  erlval  33199  orngsqr  33272  1arithufdlem3  33507  1arithufd  33509  resssra  33573  lbslelsp  33583  constrrecl  33749  constrinvcl  33753  constrsqrtcl  33759  1smat1  33781  esumcst  34040  esumrnmpt2  34045  hasheuni  34062  esumcvg  34063  ddemeas  34213  omssubadd  34278  eulerpartlemgc  34340  eulerpartlemb  34346  plymulx  34526  signswmnd  34535  pthhashvtx  35096  erdsze2lem1  35171  mrsubvrs  35490  unblimceq0lem  36470  unbdqndv2lem2  36474  knoppndvlem10  36485  wl-spae  37485  wl-cbvalnaed  37496  wl-nfeqfb  37500  unccur  37573  poimirlem15  37605  poimirlem22  37612  itg2addnclem  37641  itg2addnclem2  37642  iblmulc2nc  37655  ftc1anclem5  37667  ftc1anc  37671  dvasin  37674  areacirclem5  37682  exmid2  38069  3dim1  39432  3dim2  39433  3dim3  39434  3atlem3  39450  3atlem7  39454  lvolnle3at  39547  2lplnja  39584  paddasslem18  39802  lhpexle3lem  39976  4atex  40041  cdlemd5  40167  cdleme16  40250  cdleme20  40289  cdleme21j  40301  cdleme21  40302  cdleme32snaw  40400  cdleme32fvcl  40405  cdleme32le  40412  cdlemeg46gf  40498  cdleme48gfv  40502  cdleme50trn12  40517  cdlemg6  40588  cdlemg7N  40591  cdlemg38  40680  cdlemg46  40700  dibvalrel  41128  dihlss  41215  dihglblem5aN  41257  dihmeetbN  41268  dihmeetALTN  41292  dihatlat  41299  dihatexv  41303  dvh3dim2  41413  dvh3dim3N  41414  lclkrlem2h  41479  mapdh8d  41748  mapdh8g  41750  hdmap11lem2  41807  lcmineqlem23  42010  aks4d1p3  42037  aks4d1p5  42039  aks4d1p7d1  42041  posbezout  42059  aks6d1c2p2  42078  aks6d1c4  42083  aks6d1c5lem1  42095  aks6d1c6lem3  42131  aks6d1c6lem4  42132  bcled  42137  bcle2d  42138  aks6d1c7  42143  grpods  42153  unitscyglem2  42155  unitscyglem4  42157  aks5lem8  42160  metakunt23  42186  metakunt24  42187  metakunt29  42192  metakunt30  42193  metakunt31  42194  dffltz  42604  ttac  43007  pw2f1ocnv  43008  aomclem5  43029  isnumbasgrplem3  43076  iocmbl  43184  oe0suclim  43248  tfsconcatfv  43312  safesnsupfidom1o  43388  safesnsupfilb  43389  r1rankcld  44203  grur1cld  44204  grucollcld  44232  mnuprd  44248  radcnvrat  44286  bccbc  44317  binomcxp  44329  fnchoice  45001  fiiuncl  45037  eliin2f  45076  founiiun0  45162  axccdom  45194  axccd2  45202  fzisoeu  45277  fperiodmul  45281  upbdrech2  45285  fzdifsuc2  45287  uzfissfz  45301  supxrgere  45308  supxrgelem  45312  supxrge  45313  suplesup  45314  infrpge  45326  xrlexaddrp  45327  xralrple2  45329  infxr  45342  infleinflem1  45345  infleinflem2  45346  infleinf  45347  xralrple3  45349  xrralrecnnge  45365  uzublem  45405  supxrmnf2  45408  infxrpnf  45421  infxrpnf2  45438  supminfxr  45439  supminfxr2  45444  pimxrneun  45463  rexanuz2nf  45467  ioondisj2  45470  iccdifprioo  45493  fmul01lt1lem1  45561  fmul01lt1lem2  45562  limciccioolb  45598  lptioo2  45608  lptioo1  45609  limcicciooub  45614  lptre2pt  45617  limcresiooub  45619  limcresioolb  45620  limcleqr  45621  climfveq  45646  climfveqf  45657  limsupubuzlem  45689  limsupubuz  45690  limsupmnfuzlem  45703  limsupre3uzlem  45712  climxrre  45727  limsup10exlem  45749  cnrefiisplem  45806  climxlim2lem  45822  dfxlim2v  45824  xlimliminflimsup  45839  coskpi2  45843  cosknegpi  45846  icccncfext  45864  cncfiooicclem1  45870  cncfiooicc  45871  cncfiooiccre  45872  dvbdfbdioolem2  45906  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnxpaek  45919  dvnprodlem1  45923  dvnprodlem3  45925  volioc  45949  itgioocnicc  45954  iblcncfioo  45955  volico  45960  sublevolico  45961  ismbl3  45963  ovolsplit  45965  volioore  45967  voliooico  45969  voliccico  45976  stoweidlem14  45991  stoweidlem26  46003  stoweidlem28  46005  stoweidlem55  46032  stoweid  46040  stirlinglem5  46055  stirlinglem12  46062  dirkerper  46073  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncf  46084  fourierdlem10  46094  fourierdlem12  46096  fourierdlem24  46108  fourierdlem30  46114  fourierdlem31  46115  fourierdlem32  46116  fourierdlem33  46117  fourierdlem34  46118  fourierdlem35  46119  fourierdlem37  46121  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem43  46127  fourierdlem44  46128  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem54  46137  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem78  46161  fourierdlem79  46162  fourierdlem80  46163  fourierdlem81  46164  fourierdlem82  46165  fourierdlem92  46175  fourierdlem93  46176  fourierdlem97  46180  fourierdlem101  46184  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem109  46192  fourierdlem114  46197  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  elaa2lem  46210  etransclem15  46226  etransclem19  46230  etransclem20  46231  etransclem22  46233  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem27  46238  etransclem28  46239  etransclem35  46246  etransclem38  46249  qndenserrnbl  46272  ioorrnopn  46282  ioorrnopnxrlem  46283  ioorrnopnxr  46284  prsal  46295  salexct  46311  issalnnd  46322  sge0sn  46356  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0sup  46368  sge0less  46369  sge0pr  46371  sge0prle  46378  sge0le  46384  sge0split  46386  sge0splitmpt  46388  sge0iunmptlemfi  46390  sge0iunmpt  46395  sge0isum  46404  sge0xaddlem1  46410  sge0xadd  46412  sge0gtfsumgt  46420  nnfoctbdjlem  46432  iundjiun  46437  meadjun  46439  ismeannd  46444  voliunsge0lem  46449  meaiuninc3v  46461  caragenfiiuncl  46492  omeiunltfirp  46496  carageniuncl  46500  caragenunicl  46501  isomenndlem  46507  isomennd  46508  hoicvr  46525  ovnssle  46538  ovn0  46543  ovnsubadd  46549  hsphoidmvle2  46562  hoidmvval0b  46567  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1le  46571  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem5  46576  hoidmvle  46577  ovnhoilem1  46578  ovnhoi  46580  ovnlecvr2  46587  hspdifhsp  46593  hoidifhspdmvle  46597  hoiqssbl  46602  hspmbllem1  46603  hspmbllem2  46604  hspmbl  46606  hoimbl  46608  volico2  46618  ovolval2lem  46620  ovnsubadd2lem  46622  ovolval4lem1  46626  ovolval4lem2  46627  ovolval5lem1  46629  vonhoire  46649  iunhoiioo  46653  vonioo  46659  vonicc  46662  vonsn  46668  pimrecltpos  46685  incsmflem  46718  smfpimltxr  46724  smfconst  46726  decsmflem  46743  smfpimgtxr  46757  smfrec  46766  smfpimne2  46817  sharhght  46842  rrx2linest  48670  mofsn2  48771  ipolub00  48915  resccat  48989  initopropdlemlem  49104  prcof1  49246