Theorem pm2.61dan 825

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm2.61ddan  826  pm2.61dda  827  nfsb4t  2530  sbal2  2560  pm2.61danel  3077  ifeq1da  4517  ifeq2da  4518  ifeq12da  4519  ifclda  4521  ifeqda  4522  ifbothda  4524  2if2  4541  somin1  6131  xpcan  6173  fvmpti  6989  fvmptss  7003  funressn  7160  ovima0  7597  ordsuci  7811  suppssov1  8199  suppssov2  8200  oeoa  8589  oeoe  8591  omabs  8643  eceqoveq  8826  domdifsn  9062  pw2f1olem  9083  mapdom1  9144  marypha1lem  9407  supval2  9429  infdifsn  9640  ttrcltr  9699  ttrclselem1  9708  carden2b  9976  fidomtri  10002  dfac12lem2  10151  infunsdom1  10218  infunsdom  10219  itunisuc  10425  gchdomtri  10642  fiminre2  12191  xrmax2  13232  xrmin1  13233  ifle  13253  xnn0lem1lt  13300  xmulneg1  13325  xrsupsslem  13363  xrinfmsslem  13364  fzneuz  13667  seqf1olem1  14109  bccmpl  14377  bcval5  14386  bcpasc  14389  bccl  14390  hasheni  14416  hashfn  14443  hashdom  14447  hashdomi  14448  hashge1  14457  hashbc  14522  pfxval0  14750  sumz  15812  sumss  15814  fsumsplitsn  15834  sumsplit  15858  prod1  16037  prodss  16040  fprodsplitsn  16082  fprodle  16089  bitsmod  16532  sadadd2lem2  16546  sadcaddlem  16553  gcddvds  16599  gcdcl  16602  gcdneg  16618  dvdslcm  16694  lcmcl  16697  lcmneg  16699  lcmgcd  16703  lcmfcl  16724  dvdslcmf  16727  pcgcd  16976  pcmpt  16990  pcmpt2  16991  pcprod  16993  fldivp1  16995  prmreclem4  17017  vdwlem6  17084  ramub1lem1  17124  cidpropd  17804  rescabs  17928  lubval  18448  glbval  18461  joinval  18469  meetval  18483  acsexdimd  18653  gsumpropd2lem  18787  gsumval2  18794  mulgfval  19198  f1otrspeq  19580  pmtrfinv  19594  psgnunilem1  19626  gsumval3  20040  ablfac1c  20206  ablfac1eu  20208  mgpress  20289  orngsqr  21038  frlmsslsp  22015  psrbas  22155  resspsrbas  22194  mplmonmul  22258  mplcoe1  22259  mplcoe5  22262  opsrle  22269  opsrbaslem  22271  psrbaspropd  22465  mplbaspropd  22467  mdetdiag  22827  mdetunilem7  22846  mdetunilem9  22848  maducoeval2  22868  madurid  22872  opnnei  23351  restbas  23389  hauspwdom  23733  ptcmplem5  24288  xrsmopn  25045  xrhmeo  25180  lebnum  25198  pcoass  25258  pcorevlem  25260  icombl  25798  ioombl  25799  mbfconstlem  25861  mbfima  25864  i1fd  25915  mbfi1fseqlem5  25953  itg2const2  25975  itg2seq  25976  itg2uba  25977  itg2splitlem  25982  itg2split  25983  itg2monolem1  25984  itg2gt0  25994  itg2cnlem1  25995  itg2cnlem2  25996  iblss  26039  iblss2  26040  itgss  26046  bddmulibl  26073  coemullem  26483  plymulidp  26519  aaliou2b  26584  isppw2  27359  mule1  27392  ppip1le  27405  dchrelbas3  27482  dchrpt  27511  bposlem3  27530  bposlem5  27532  bposlem6  27533  lgslem4  27544  lgsneg  27565  lgsmod  27567  lgsdilem  27568  lgsdir  27576  lgsdi  27578  lgsne0  27579  lgsquad3  27631  dchrvmasum2if  27741  maxs2  28014  mins1  28015  z12bday  28758  tglnpt4  29010  midexlem  29051  colperpex  29096  outpasch  29120  hlpasch  29121  lnopp2hpgb  29128  lmieu  29176  perpeq  29235  tgaaddcpbl  29239  inaghl  29251  cgrg3col4  29259  angmgmaddov1lem  29273  angmgmaddrid  29280  perpprlng  29315  prlngex  29316  prlngmo2  29321  pthhashvtx  30202  pthdlem1  30239  nmcfnlbi  32541  elpreq  33011  prssad  33012  prssbd  33013  disjdifprg  33056  disjun0  33076  argcj  33227  f1ocnt  33279  xrge0npcan  33468  psgnfzto1stlem  33548  cyc3genpmlem  33599  cyc3conja  33605  archiabl  33646  erlval  33706  1arithufdlem3  33964  1arithufd  33966  psrmonmul  34068  esplyfval3  34090  resssra  34105  lbslelsp  34116  constrrecl  34287  constrinvcl  34291  constrsqrtcl  34297  1smat1  34322  esumcst  34581  esumrnmpt2  34586  hasheuni  34603  esumcvg  34604  ddemeas  34755  omssubadd  34819  eulerpartlemgc  34881  eulerpartlemb  34887  signswmnd  35073  fineqvnttrclselem1  35655  erdsze2lem1  35790  mrsubvrs  36109  unblimceq0lem  37211  unbdqndv2lem2  37215  knoppndvlem10  37226  wl-spae  38292  wl-cbvalnaed  38303  wl-nfeqfb  38307  unccur  38365  poimirlem15  38392  poimirlem22  38399  itg2addnclem  38428  itg2addnclem2  38429  iblmulc2nc  38442  ftc1anclem5  38454  ftc1anc  38458  dvasin  38461  areacirclem5  38469  exmid2  38855  3dim1  40348  3dim2  40349  3dim3  40350  3atlem3  40366  3atlem7  40370  lvolnle3at  40463  2lplnja  40500  paddasslem18  40718  lhpexle3lem  40892  4atex  40957  cdlemd5  41083  cdleme16  41166  cdleme20  41205  cdleme21j  41217  cdleme21  41218  cdleme32snaw  41316  cdleme32fvcl  41321  cdleme32le  41328  cdlemeg46gf  41414  cdleme48gfv  41418  cdleme50trn12  41433  cdlemg6  41504  cdlemg7N  41507  cdlemg38  41596  cdlemg46  41616  dibvalrel  42044  dihlss  42131  dihglblem5aN  42173  dihmeetbN  42184  dihmeetALTN  42208  dihatlat  42215  dihatexv  42219  dvh3dim2  42329  dvh3dim3N  42330  lclkrlem2h  42395  mapdh8d  42664  mapdh8g  42666  hdmap11lem2  42723  lcmineqlem23  42925  aks4d1p3  42952  aks4d1p5  42954  aks4d1p7d1  42956  posbezout  42974  aks6d1c2p2  42993  aks6d1c4  42998  aks6d1c5lem1  43010  aks6d1c6lem3  43046  aks6d1c6lem4  43047  bcled  43052  bcle2d  43053  aks6d1c7  43058  grpods  43068  unitscyglem2  43070  unitscyglem4  43072  aks5lem8  43075  dffltz  43488  ttac  43885  pw2f1ocnv  43886  aomclem5  43907  isnumbasgrplem3  43954  iocmbl  44062  oe0suclim  44126  tfsconcatfv  44190  safesnsupfidom1o  44265  safesnsupfilb  44266  r1rankcld  45077  grur1cld  45078  grucollcld  45092  mnuprd  45108  radcnvrat  45146  bccbc  45177  binomcxp  45189  fnchoice  45871  fiiuncl  45907  eliin2f  45944  founiiun0  46030  axccdom  46060  axccd2  46067  fzisoeu  46141  fperiodmul  46145  upbdrech2  46149  fzdifsuc2  46151  uzfissfz  46164  supxrgere  46171  supxrgelem  46175  supxrge  46176  suplesup  46177  infrpge  46189  xrlexaddrp  46190  xralrple2  46192  infxr  46204  infleinflem1  46207  infleinflem2  46208  infleinf  46209  xralrple3  46211  xrralrecnnge  46227  uzublem  46266  supxrmnf2  46269  infxrpnf  46282  infxrpnf2  46299  supminfxr  46300  supminfxr2  46305  pimxrneun  46324  rexanuz2nf  46328  ioondisj2  46331  iccdifprioo  46354  fmul01lt1lem1  46422  fmul01lt1lem2  46423  limciccioolb  46459  lptioo2  46469  lptioo1  46470  limcicciooub  46473  lptre2pt  46476  limcresiooub  46478  limcresioolb  46479  limcleqr  46480  climfveq  46505  climfveqf  46516  limsupubuzlem  46548  limsupubuz  46549  limsupmnfuzlem  46562  limsupre3uzlem  46571  climxrre  46586  limsup10exlem  46608  cnrefiisplem  46665  climxlim2lem  46681  dfxlim2v  46683  xlimliminflimsup  46698  coskpi2  46702  cosknegpi  46705  icccncfext  46723  cncfiooicclem1  46729  cncfiooicc  46730  cncfiooiccre  46731  dvbdfbdioolem2  46765  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnxpaek  46778  dvnprodlem1  46782  dvnprodlem3  46784  volioc  46808  itgioocnicc  46813  iblcncfioo  46814  volico  46819  sublevolico  46820  ismbl3  46822  ovolsplit  46824  volioore  46826  voliooico  46828  voliccico  46835  stoweidlem14  46850  stoweidlem26  46862  stoweidlem28  46864  stoweidlem55  46891  stoweid  46899  stirlinglem5  46914  stirlinglem12  46921  dirkerper  46932  dirkertrigeqlem3  46936  dirkertrigeq  46937  dirkercncflem1  46939  dirkercncflem2  46940  dirkercncf  46943  fourierdlem10  46953  fourierdlem12  46955  fourierdlem24  46967  fourierdlem30  46973  fourierdlem31  46974  fourierdlem32  46975  fourierdlem33  46976  fourierdlem34  46977  fourierdlem35  46978  fourierdlem37  46980  fourierdlem40  46983  fourierdlem41  46984  fourierdlem42  46985  fourierdlem43  46986  fourierdlem44  46987  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem51  46993  fourierdlem54  46996  fourierdlem62  47004  fourierdlem64  47006  fourierdlem65  47007  fourierdlem70  47012  fourierdlem71  47013  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem78  47020  fourierdlem79  47021  fourierdlem80  47022  fourierdlem81  47023  fourierdlem82  47024  fourierdlem92  47034  fourierdlem93  47035  fourierdlem97  47039  fourierdlem101  47043  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem109  47051  fourierdlem114  47056  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  elaa2lem  47069  etransclem15  47085  etransclem19  47089  etransclem20  47090  etransclem22  47092  etransclem23  47093  etransclem24  47094  etransclem25  47095  etransclem27  47097  etransclem28  47098  etransclem35  47105  etransclem38  47108  qndenserrnbl  47131  ioorrnopn  47141  ioorrnopnxrlem  47142  ioorrnopnxr  47143  prsal  47154  salexct  47170  issalnnd  47181  sge0sn  47215  sge0tsms  47216  sge0cl  47217  sge0f1o  47218  sge0sup  47227  sge0less  47228  sge0pr  47230  sge0prle  47237  sge0le  47243  sge0split  47245  sge0splitmpt  47247  sge0iunmptlemfi  47249  sge0iunmpt  47254  sge0isum  47263  sge0xaddlem1  47269  sge0xadd  47271  sge0gtfsumgt  47279  nnfoctbdjlem  47291  iundjiun  47296  meadjun  47298  ismeannd  47303  voliunsge0lem  47308  meaiuninc3v  47320  caragenfiiuncl  47351  omeiunltfirp  47355  carageniuncl  47359  caragenunicl  47360  isomenndlem  47366  isomennd  47367  hoicvr  47384  ovnssle  47397  ovn0  47402  ovnsubadd  47408  hsphoidmvle2  47421  hoidmvval0b  47426  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmv1le  47430  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem5  47435  hoidmvle  47436  ovnhoilem1  47437  ovnhoi  47439  ovnlecvr2  47446  hspdifhsp  47452  hoidifhspdmvle  47456  hoiqssbl  47461  hspmbllem1  47462  hspmbllem2  47463  hspmbl  47465  hoimbl  47467  volico2  47477  ovolval2lem  47479  ovnsubadd2lem  47481  ovolval4lem1  47485  ovolval4lem2  47486  ovolval5lem1  47488  vonhoire  47508  iunhoiioo  47512  vonioo  47518  vonicc  47521  vonsn  47527  pimrecltpos  47544  incsmflem  47577  smfpimltxr  47583  smfconst  47585  decsmflem  47602  smfpimgtxr  47616  smfrec  47625  smfpimne2  47676  sharhght  47701  tmachlem-agreeprod  47773  rrx2linest  49680  mofsn2  49781  ipolub00  49927  resccat  50008  initopropdlemlem  50173  prcof1  50322