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  2498  sbal2  2528  pm2.61danel  3044  ifeq1da  4523  ifeq2da  4524  ifeq12da  4525  ifclda  4527  ifeqda  4528  ifbothda  4530  2if2  4547  somin1  6109  xpcan  6152  fvmpti  6970  fvmptss  6983  funressn  7134  ovima0  7571  ordsuci  7787  suppssov1  8179  suppssov2  8180  oeoa  8564  oeoe  8566  omabs  8618  eceqoveq  8798  domdifsn  9028  pw2f1olem  9050  mapdom1  9112  imafiOLD  9272  marypha1lem  9391  supval2  9413  infdifsn  9617  ttrcltr  9676  ttrclselem1  9685  carden2b  9927  fidomtri  9953  dfac12lem2  10105  infunsdom1  10172  infunsdom  10173  itunisuc  10379  gchdomtri  10589  fiminre2  12138  xrmax2  13143  xrmin1  13144  ifle  13164  xnn0lem1lt  13211  xmulneg1  13236  xrsupsslem  13274  xrinfmsslem  13275  fzneuz  13576  seqf1olem1  14013  bccmpl  14281  bcval5  14290  bcpasc  14293  bccl  14294  hasheni  14320  hashfn  14347  hashdom  14351  hashdomi  14352  hashge1  14361  hashbc  14425  pfxval0  14648  sumz  15695  sumss  15697  fsumsplitsn  15717  sumsplit  15741  prod1  15917  prodss  15920  fprodsplitsn  15962  fprodle  15969  bitsmod  16413  sadadd2lem2  16427  sadcaddlem  16434  gcddvds  16480  gcdcl  16483  gcdneg  16499  dvdslcm  16575  lcmcl  16578  lcmneg  16580  lcmgcd  16584  lcmfcl  16605  dvdslcmf  16608  pcgcd  16856  pcmpt  16870  pcmpt2  16871  pcprod  16873  fldivp1  16875  prmreclem4  16897  vdwlem6  16964  ramub1lem1  17004  cidpropd  17678  rescabs  17802  lubval  18322  glbval  18335  joinval  18343  meetval  18357  acsexdimd  18525  gsumpropd2lem  18613  gsumval2  18620  mulgfval  19008  f1otrspeq  19384  pmtrfinv  19398  psgnunilem1  19430  gsumval3  19844  ablfac1c  20010  ablfac1eu  20012  mgpress  20066  frlmsslsp  21712  psrbas  21849  resspsrbas  21890  mplmonmul  21950  mplcoe1  21951  mplcoe5  21954  opsrle  21961  opsrbaslem  21963  psrbaspropd  22126  mplbaspropd  22128  mdetdiag  22493  mdetunilem7  22512  mdetunilem9  22514  maducoeval2  22534  madurid  22538  opnnei  23014  restbas  23052  hauspwdom  23395  ptcmplem5  23950  xrsmopn  24708  xrhmeo  24851  lebnum  24870  pcoass  24931  pcorevlem  24933  icombl  25472  ioombl  25473  mbfconstlem  25535  mbfima  25538  i1fd  25589  mbfi1fseqlem5  25627  itg2const2  25649  itg2seq  25650  itg2uba  25651  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  iblss2  25714  itgss  25720  bddmulibl  25747  coemullem  26162  aaliou2b  26256  isppw2  27032  mule1  27065  ppip1le  27078  dchrelbas3  27156  dchrpt  27185  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgslem4  27218  lgsneg  27239  lgsmod  27241  lgsdilem  27242  lgsdir  27250  lgsdi  27252  lgsne0  27253  lgsquad3  27305  dchrvmasum2if  27415  maxs2  27685  mins1  27686  midexlem  28626  colperpex  28667  outpasch  28689  hlpasch  28690  lnopp2hpgb  28697  lmieu  28718  inaghl  28779  cgrg3col4  28787  pthdlem1  29703  nmcfnlbi  31988  elpreq  32464  prssad  32465  prssbd  32466  disjdifprg  32511  disjun0  32531  argcj  32679  f1ocnt  32732  xrge0npcan  32968  psgnfzto1stlem  33064  cyc3genpmlem  33115  cyc3conja  33121  archiabl  33159  erlval  33216  orngsqr  33289  1arithufdlem3  33524  1arithufd  33526  resssra  33590  lbslelsp  33600  constrrecl  33766  constrinvcl  33770  constrsqrtcl  33776  1smat1  33801  esumcst  34060  esumrnmpt2  34065  hasheuni  34082  esumcvg  34083  ddemeas  34233  omssubadd  34298  eulerpartlemgc  34360  eulerpartlemb  34366  plymulx  34546  signswmnd  34555  pthhashvtx  35122  erdsze2lem1  35197  mrsubvrs  35516  unblimceq0lem  36501  unbdqndv2lem2  36505  knoppndvlem10  36516  wl-spae  37516  wl-cbvalnaed  37527  wl-nfeqfb  37531  unccur  37604  poimirlem15  37636  poimirlem22  37643  itg2addnclem  37672  itg2addnclem2  37673  iblmulc2nc  37686  ftc1anclem5  37698  ftc1anc  37702  dvasin  37705  areacirclem5  37713  exmid2  38100  3dim1  39468  3dim2  39469  3dim3  39470  3atlem3  39486  3atlem7  39490  lvolnle3at  39583  2lplnja  39620  paddasslem18  39838  lhpexle3lem  40012  4atex  40077  cdlemd5  40203  cdleme16  40286  cdleme20  40325  cdleme21j  40337  cdleme21  40338  cdleme32snaw  40436  cdleme32fvcl  40441  cdleme32le  40448  cdlemeg46gf  40534  cdleme48gfv  40538  cdleme50trn12  40553  cdlemg6  40624  cdlemg7N  40627  cdlemg38  40716  cdlemg46  40736  dibvalrel  41164  dihlss  41251  dihglblem5aN  41293  dihmeetbN  41304  dihmeetALTN  41328  dihatlat  41335  dihatexv  41339  dvh3dim2  41449  dvh3dim3N  41450  lclkrlem2h  41515  mapdh8d  41784  mapdh8g  41786  hdmap11lem2  41843  lcmineqlem23  42046  aks4d1p3  42073  aks4d1p5  42075  aks4d1p7d1  42077  posbezout  42095  aks6d1c2p2  42114  aks6d1c4  42119  aks6d1c5lem1  42131  aks6d1c6lem3  42167  aks6d1c6lem4  42168  bcled  42173  bcle2d  42174  aks6d1c7  42179  grpods  42189  unitscyglem2  42191  unitscyglem4  42193  aks5lem8  42196  dffltz  42629  ttac  43032  pw2f1ocnv  43033  aomclem5  43054  isnumbasgrplem3  43101  iocmbl  43209  oe0suclim  43273  tfsconcatfv  43337  safesnsupfidom1o  43413  safesnsupfilb  43414  r1rankcld  44227  grur1cld  44228  grucollcld  44256  mnuprd  44272  radcnvrat  44310  bccbc  44341  binomcxp  44353  fnchoice  45030  fiiuncl  45066  eliin2f  45105  founiiun0  45191  axccdom  45223  axccd2  45231  fzisoeu  45305  fperiodmul  45309  upbdrech2  45313  fzdifsuc2  45315  uzfissfz  45329  supxrgere  45336  supxrgelem  45340  supxrge  45341  suplesup  45342  infrpge  45354  xrlexaddrp  45355  xralrple2  45357  infxr  45370  infleinflem1  45373  infleinflem2  45374  infleinf  45375  xralrple3  45377  xrralrecnnge  45393  uzublem  45433  supxrmnf2  45436  infxrpnf  45449  infxrpnf2  45466  supminfxr  45467  supminfxr2  45472  pimxrneun  45491  rexanuz2nf  45495  ioondisj2  45498  iccdifprioo  45521  fmul01lt1lem1  45589  fmul01lt1lem2  45590  limciccioolb  45626  lptioo2  45636  lptioo1  45637  limcicciooub  45642  lptre2pt  45645  limcresiooub  45647  limcresioolb  45648  limcleqr  45649  climfveq  45674  climfveqf  45685  limsupubuzlem  45717  limsupubuz  45718  limsupmnfuzlem  45731  limsupre3uzlem  45740  climxrre  45755  limsup10exlem  45777  cnrefiisplem  45834  climxlim2lem  45850  dfxlim2v  45852  xlimliminflimsup  45867  coskpi2  45871  cosknegpi  45874  icccncfext  45892  cncfiooicclem1  45898  cncfiooicc  45899  cncfiooiccre  45900  dvbdfbdioolem2  45934  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnxpaek  45947  dvnprodlem1  45951  dvnprodlem3  45953  volioc  45977  itgioocnicc  45982  iblcncfioo  45983  volico  45988  sublevolico  45989  ismbl3  45991  ovolsplit  45993  volioore  45995  voliooico  45997  voliccico  46004  stoweidlem14  46019  stoweidlem26  46031  stoweidlem28  46033  stoweidlem55  46060  stoweid  46068  stirlinglem5  46083  stirlinglem12  46090  dirkerper  46101  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncf  46112  fourierdlem10  46122  fourierdlem12  46124  fourierdlem24  46136  fourierdlem30  46142  fourierdlem31  46143  fourierdlem32  46144  fourierdlem33  46145  fourierdlem34  46146  fourierdlem35  46147  fourierdlem37  46149  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem43  46155  fourierdlem44  46156  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem54  46165  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem79  46190  fourierdlem80  46191  fourierdlem81  46192  fourierdlem82  46193  fourierdlem92  46203  fourierdlem93  46204  fourierdlem97  46208  fourierdlem101  46212  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem109  46220  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  etransclem15  46254  etransclem19  46258  etransclem20  46259  etransclem22  46261  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem27  46266  etransclem28  46267  etransclem35  46274  etransclem38  46277  qndenserrnbl  46300  ioorrnopn  46310  ioorrnopnxrlem  46311  ioorrnopnxr  46312  prsal  46323  salexct  46339  issalnnd  46350  sge0sn  46384  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0sup  46396  sge0less  46397  sge0pr  46399  sge0prle  46406  sge0le  46412  sge0split  46414  sge0splitmpt  46416  sge0iunmptlemfi  46418  sge0iunmpt  46423  sge0isum  46432  sge0xaddlem1  46438  sge0xadd  46440  sge0gtfsumgt  46448  nnfoctbdjlem  46460  iundjiun  46465  meadjun  46467  ismeannd  46472  voliunsge0lem  46477  meaiuninc3v  46489  caragenfiiuncl  46520  omeiunltfirp  46524  carageniuncl  46528  caragenunicl  46529  isomenndlem  46535  isomennd  46536  hoicvr  46553  ovnssle  46566  ovn0  46571  ovnsubadd  46577  hsphoidmvle2  46590  hoidmvval0b  46595  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem1  46606  ovnhoi  46608  ovnlecvr2  46615  hspdifhsp  46621  hoidifhspdmvle  46625  hoiqssbl  46630  hspmbllem1  46631  hspmbllem2  46632  hspmbl  46634  hoimbl  46636  volico2  46646  ovolval2lem  46648  ovnsubadd2lem  46650  ovolval4lem1  46654  ovolval4lem2  46655  ovolval5lem1  46657  vonhoire  46677  iunhoiioo  46681  vonioo  46687  vonicc  46690  vonsn  46696  pimrecltpos  46713  incsmflem  46746  smfpimltxr  46752  smfconst  46754  decsmflem  46771  smfpimgtxr  46785  smfrec  46794  smfpimne2  46845  sharhght  46870  rrx2linest  48735  mofsn2  48837  ipolub00  48985  resccat  49067  initopropdlemlem  49232  prcof1  49381