Theorem pm2.61dane 3026

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)

Hypotheses

Ref	Expression
pm2.61dane.1	⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
pm2.61dane.2	⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)

Assertion

Ref	Expression
pm2.61dane	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.61dane

Step	Hyp	Ref	Expression
1		pm2.61dane.1	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
2	1	ex 412	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 412	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3025	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ≠ wne 2937

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  df-ne 2938

This theorem is referenced by:  pm2.61da2ne  3027  pm2.61da3ne  3028  pm2.61iine  3029  disjxiun  5144  onfr  6424  f1oprswap  6892  soex  7943  frxp2  8167  frxp3  8174  riiner  8828  difsnen  9091  mapdom2  9186  nnunifi  9324  fofinf1o  9369  brwdom2  9610  cantnff  9711  cantnfp1  9718  carddomi2  10007  wdomfil  10098  fin1a2lem10  10446  fin1a2lem11  10447  uzsupss  12979  xaddcom  13278  xnegdi  13286  xpncan  13289  xleadd1a  13291  xsubge0  13299  ccat1st1st  14662  swrdccatin1  14759  cnpart  15275  fsumcllem  15764  fsumrev2  15814  expcnv  15896  geomulcvg  15908  fprodcllem  15983  fsumdvds  16341  gcd0id  16552  nn0seqcvgd  16603  lcmdvds  16641  mulgcddvds  16688  pcge0  16895  pcneg  16907  pcdvdstr  16909  pcz  16914  pcprmpw2  16915  pcadd  16922  ramcl2  17049  0ramcl  17056  ramub1lem1  17059  ramcl  17062  mrerintcl  17641  mreriincl  17642  mreexexlem4d  17691  mreclatBAD  18620  psgnunilem1  19525  odmulg  19588  sylow1lem1  19630  pgpfi  19637  odadd1  19880  odadd2  19881  gsumval3  19939  gsumpt  19994  dprdfcntz  20049  dprd2da  20076  ablfac1eulem  20106  pgpfaclem3  20117  ablsimpgfind  20144  abvneg  20843  lssssr  20969  lspsneq  21141  lspdisj2  21146  drngnidl  21270  cnsubrg  21462  riinopn  22929  riincld  23067  neipeltop  23152  hauscmplem  23429  cmpfi  23431  ptbasfi  23604  xkoccn  23642  txindislem  23656  txtube  23663  hmphindis  23820  fclscmp  24053  utop2nei  24274  nrginvrcn  24728  nmoleub  24767  blcvx  24833  xrsxmet  24844  xrsblre  24846  lebnumlem3  25008  cphsqrtcl2  25233  ovollb2  25537  ioorcl  25625  i1fmulc  25752  itg1mulc  25753  mbfi1fseqlem4  25767  bddiblnc  25891  dvlip  26046  dvne0  26064  ig1pdvds  26233  plyeq0lem  26263  plyeq0  26264  aannenlem2  26385  aalioulem6  26393  abelthlem8  26497  abelth  26499  cxpexp  26724  cxpge0  26739  cxpmul2  26745  abscxp2  26749  abscxpbnd  26810  cxpeq  26814  nnlogbexp  26838  isosctrlem2  26876  atanrecl  26968  wilthlem2  27126  dchrabs2  27320  dchr1re  27321  lgsneg1  27380  lgsdirprm  27389  lgsdir  27390  lgsne0  27393  lgsdirnn0  27402  lgsdinn0  27403  2sqlem9  27485  rpvmasumlem  27545  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  rpvmasum2  27570  pntrsumbnd2  27625  pntleml  27669  tgcgrextend  28507  tgbtwnexch2  28518  tgifscgr  28530  tgcolg  28576  tgidinside  28593  tgbtwnconn1lem2  28595  tgbtwnconn1lem3  28596  lnhl  28637  tglinethru  28658  tglnpt2  28663  tglineneq  28666  coltr  28669  coltr3  28670  colline  28671  mirreu3  28676  miriso  28692  mirln  28698  mirln2  28699  mirconn  28700  mirbtwnhl  28702  colmid  28710  krippenlem  28712  midexlem  28714  ragflat  28726  ragcgr  28729  perprag  28748  perpdragALT  28749  colperpexlem1  28752  colperpexlem3  28754  midex  28759  opphllem1  28769  opphllem2  28770  opphllem5  28773  opphllem6  28774  hlpasch  28778  lmiisolem  28818  hypcgrlem1  28821  hypcgrlem2  28822  cgrg3col4  28875  upgrex  29123  crctcshwlk  29851  crctcsh  29853  1wlkdlem2  30166  eupth2lem3lem3  30258  eupth2lem3lem7  30262  nmcoplbi  32056  nmophmi  32059  nmbdfnlbi  32077  disjdifprg  32594  imadifxp  32620  2ndimaxp  32662  mptiffisupp  32707  xlt2addrd  32768  ssnnssfz  32795  chnub  32985  gsumpart  33042  symgcntz  33087  fzo0pmtrlast  33094  pmtridf1o  33096  pmtridfv1  33097  pmtridfv2  33098  psgnfzto1stlem  33102  tocycf  33119  cycpmco2lem5  33132  cycpmco2  33135  linds2eq  33388  dvdsruasso  33392  ply1degltel  33594  ply1degleel  33595  ig1pmindeg  33601  fldext2chn  33733  locfinref  33801  zarcmplem  33841  esumpr2  34047  unelldsys  34138  sigapildsyslem  34141  sigapildsys  34142  mbfmcst  34240  carsgsigalem  34296  carsgclctunlem3  34301  pmeasmono  34305  probun  34400  0rrv  34432  sgncl  34519  signsvtn0  34563  signstfvneq0  34565  fineqvac  35089  wevgblacfn  35092  btwnconn1lem11  36078  finxp00  37384  matunitlindf  37604  poimirlem14  37620  mblfinlem1  37643  mblfinlem2  37644  ismblfin  37647  itg2addnclem  37657  itgaddnclem2  37665  areacirclem4  37697  areacirc  37699  isbnd3  37770  blbnd  37773  rrnequiv  37821  lsmsat  38989  lkrscss  39079  eqlkr  39080  lkrshpor  39088  atcvrj2b  39414  atltcvr  39417  3dim1  39449  3dim2  39450  3dim3  39451  ps-2  39460  2at0mat0  39507  dalemdnee  39648  dalem63  39717  lnatexN  39761  2llnma3r  39770  pmodlem1  39828  pmapjat1  39835  pclfinclN  39932  osumclN  39949  pexmidALTN  39960  lhpexle2lem  39991  lhpexle3lem  39993  4atexlemex6  40056  4atex  40058  trlnle  40168  trlval3  40169  cdlemc  40179  cdlemd9  40188  cdleme27N  40351  cdleme28c  40354  cdleme32fvaw  40421  cdleme42ke  40467  cdleme42keg  40468  cdleme42mgN  40470  cdleme17d  40480  cdleme48fvg  40482  cdleme50trn123  40536  cdlemb3  40588  cdlemg8  40613  cdlemg15a  40637  cdlemg15  40638  cdlemg16  40639  cdlemg16ALTN  40640  cdlemg16z  40641  cdlemg16zz  40642  cdlemg20  40667  cdlemg22  40669  cdlemg37  40671  cdlemg31d  40682  cdlemg39  40698  cdlemg40  40699  ltrncom  40720  tendotr  40812  cdlemk25-3  40886  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk53b  40938  cdlemk53  40939  cdlemk55  40943  cdlemk35u  40946  cdlemk55u  40948  cdlemk39u  40950  cdlemk19u  40952  cdleml5N  40962  dia2dimlem7  41052  dia2dimlem13  41058  dih1dimatlem  41311  dihlsprn  41313  dihjat1lem  41410  dihjat1  41411  dvh2dim  41427  dochexmid  41450  lclkrlem1  41488  lclkrlem2i  41497  lclkrlem2t  41508  lcfrlem34  41558  lcfrlem38  41562  lcfrlem41  41565  mapdindp1  41702  mapdindp2  41703  mapdh6dN  41721  mapdh6jN  41727  mapdh8j  41769  mapdh8  41770  hdmap1l6d  41795  hdmap1l6j  41801  hdmap11lem2  41824  hdmap14lem7  41856  primrootlekpowne0  42086  aks6d1c7lem2  42162  unitscyglem4  42179  jm2.19  42981  jm2.23  42984  nzss  44312  disjxp1  45008  cnrefiisplem  45784  xlimliminflimsup  45817  stoweidlem58  46013  fourierdlem41  46103  fourierdlem48  46109  fouriersw  46186  etransclem24  46213  nnfoctbdjlem  46410  smfpimltxr  46702  smfpimgtxr  46735  ssnn0ssfz  48193  mreclat  48785