Theorem pm2.61dane 3106

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 415	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 415	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3105	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ≠ wne 3018

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 209  df-an 399  df-ne 3019

This theorem is referenced by:  pm2.61da2ne  3107  pm2.61da3ne  3108  pm2.61iine  3109  disjxiun  5065  onfr  6232  f1oprswap  6660  soex  7628  riiner  8372  difsnen  8601  mapdom2  8690  nnunifi  8771  fofinf1o  8801  brwdom2  9039  cantnff  9139  cantnfp1  9146  carddomi2  9401  wdomfil  9489  fin1a2lem10  9833  fin1a2lem11  9834  uzsupss  12343  xaddcom  12636  xnegdi  12644  xpncan  12647  xleadd1a  12649  xsubge0  12657  ccat1st1st  13986  swrdccatin1  14089  cnpart  14601  fsumcllem  15091  fsumrev2  15139  expcnv  15221  geomulcvg  15234  fprodcllem  15307  fsumdvds  15660  gcd0id  15869  nn0seqcvgd  15916  lcmdvds  15954  mulgcddvds  16001  pcge0  16200  pcneg  16212  pcdvdstr  16214  pcz  16219  pcprmpw2  16220  pcadd  16227  ramcl2  16354  0ramcl  16361  ramub1lem1  16364  ramcl  16367  mrerintcl  16870  mreriincl  16871  mreexexlem4d  16920  mreclatBAD  17799  psgnunilem1  18623  odmulg  18685  sylow1lem1  18725  pgpfi  18732  odadd1  18970  odadd2  18971  gsumval3  19029  gsumpt  19084  dprdfcntz  19139  dprd2da  19166  ablfac1eulem  19196  pgpfaclem3  19207  ablsimpgfind  19234  abvneg  19607  lssssr  19727  lspsneq  19896  lspdisj2  19901  drngnidl  20004  cnsubrg  20607  riinopn  21518  riincld  21654  neipeltop  21739  hauscmplem  22016  cmpfi  22018  ptbasfi  22191  xkoccn  22229  txindislem  22243  txtube  22250  hmphindis  22407  fclscmp  22640  utop2nei  22861  nrginvrcn  23303  nmoleub  23342  blcvx  23408  xrsxmet  23419  xrsblre  23421  lebnumlem3  23569  cphsqrtcl2  23792  ovollb2  24092  ioorcl  24180  i1fmulc  24306  itg1mulc  24307  mbfi1fseqlem4  24321  dvlip  24592  dvne0  24610  ig1pdvds  24772  plyeq0lem  24802  plyeq0  24803  aannenlem2  24920  aalioulem6  24928  abelthlem8  25029  abelth  25031  cxpexp  25253  cxpge0  25268  cxpmul2  25274  abscxp2  25278  abscxpbnd  25336  cxpeq  25340  nnlogbexp  25361  isosctrlem2  25399  atanrecl  25491  wilthlem2  25648  dchrabs2  25840  dchr1re  25841  lgsneg1  25900  lgsdirprm  25909  lgsdir  25910  lgsne0  25913  lgsdirnn0  25922  lgsdinn0  25923  2sqlem9  26005  rpvmasumlem  26065  dchrvmasumiflem1  26079  dchrisum0flblem1  26086  rpvmasum2  26090  pntrsumbnd2  26145  pntleml  26189  tgcgrextend  26273  tgbtwnexch2  26284  tgifscgr  26296  tgcolg  26342  tgidinside  26359  tgbtwnconn1lem2  26361  tgbtwnconn1lem3  26362  lnhl  26403  tglinethru  26424  tglnpt2  26429  tglineneq  26432  coltr  26435  coltr3  26436  colline  26437  mirreu3  26442  miriso  26458  mirln  26464  mirln2  26465  mirconn  26466  mirbtwnhl  26468  colmid  26476  krippenlem  26478  midexlem  26480  ragflat  26492  ragcgr  26495  perprag  26514  perpdragALT  26515  colperpexlem1  26518  colperpexlem3  26520  midex  26525  opphllem1  26535  opphllem2  26536  opphllem5  26539  opphllem6  26540  hlpasch  26544  lmiisolem  26584  hypcgrlem1  26587  hypcgrlem2  26588  cgrg3col4  26641  upgrex  26879  crctcshwlk  27602  crctcsh  27604  1wlkdlem2  27919  eupth2lem3lem3  28011  eupth2lem3lem7  28015  nmcoplbi  29807  nmophmi  29810  nmbdfnlbi  29828  disjdifprg  30327  imadifxp  30353  xlt2addrd  30484  ssnnssfz  30512  symgcntz  30731  pmtridf1o  30738  pmtridfv1  30739  pmtridfv2  30740  psgnfzto1stlem  30744  tocycf  30761  cycpmco2lem5  30774  cycpmco2  30777  linds2eq  30943  locfinref  31107  esumpr2  31328  unelldsys  31419  sigapildsyslem  31422  sigapildsys  31423  mbfmcst  31519  carsgsigalem  31575  carsgclctunlem3  31580  pmeasmono  31584  probun  31679  0rrv  31711  sgncl  31798  signsvtn0  31842  signstfvneq0  31844  btwnconn1lem11  33560  finxp00  34685  matunitlindf  34892  poimirlem14  34908  mblfinlem1  34931  mblfinlem2  34932  ismblfin  34935  itg2addnclem  34945  itgaddnclem2  34953  bddiblnc  34964  areacirclem4  34987  areacirc  34989  isbnd3  35064  blbnd  35067  rrnequiv  35115  lsmsat  36146  lkrscss  36236  eqlkr  36237  lkrshpor  36245  atcvrj2b  36570  atltcvr  36573  3dim1  36605  3dim2  36606  3dim3  36607  ps-2  36616  2at0mat0  36663  dalemdnee  36804  dalem63  36873  lnatexN  36917  2llnma3r  36926  pmodlem1  36984  pmapjat1  36991  pclfinclN  37088  osumclN  37105  pexmidALTN  37116  lhpexle2lem  37147  lhpexle3lem  37149  4atexlemex6  37212  4atex  37214  trlnle  37324  trlval3  37325  cdlemc  37335  cdlemd9  37344  cdleme27N  37507  cdleme28c  37510  cdleme32fvaw  37577  cdleme42ke  37623  cdleme42keg  37624  cdleme42mgN  37626  cdleme17d  37636  cdleme48fvg  37638  cdleme50trn123  37692  cdlemb3  37744  cdlemg8  37769  cdlemg15a  37793  cdlemg15  37794  cdlemg16  37795  cdlemg16ALTN  37796  cdlemg16z  37797  cdlemg16zz  37798  cdlemg20  37823  cdlemg22  37825  cdlemg37  37827  cdlemg31d  37838  cdlemg39  37854  cdlemg40  37855  ltrncom  37876  tendotr  37968  cdlemk25-3  38042  cdlemk35s-id  38076  cdlemk39s-id  38078  cdlemk53b  38094  cdlemk53  38095  cdlemk55  38099  cdlemk35u  38102  cdlemk55u  38104  cdlemk39u  38106  cdlemk19u  38108  cdleml5N  38118  dia2dimlem7  38208  dia2dimlem13  38214  dih1dimatlem  38467  dihlsprn  38469  dihjat1lem  38566  dihjat1  38567  dvh2dim  38583  dochexmid  38606  lclkrlem1  38644  lclkrlem2i  38653  lclkrlem2t  38664  lcfrlem34  38714  lcfrlem38  38718  lcfrlem41  38721  mapdindp1  38858  mapdindp2  38859  mapdh6dN  38877  mapdh6jN  38883  mapdh8j  38925  mapdh8  38926  hdmap1l6d  38951  hdmap1l6j  38957  hdmap11lem2  38980  hdmap14lem7  39012  jm2.19  39597  jm2.23  39600  nzss  40656  disjxp1  41338  cnrefiisplem  42117  xlimliminflimsup  42150  stoweidlem58  42350  fourierdlem41  42440  fourierdlem48  42446  fouriersw  42523  etransclem24  42550  nnfoctbdjlem  42744  ssnn0ssfz  44404