Theorem pm2.61dane 3048

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2961

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

This theorem is used by:  pm2.61da2ne  3049  pm2.61da3ne  3050  pm2.61iine  3051  disjxiun  5111  onfr  6407  f1oprswap  6873  soex  7927  frxp2  8149  frxp3  8156  riiner  8797  difsnen  9057  mapdom2  9146  nnunifi  9261  fofinf1o  9299  brwdom2  9545  cantnff  9653  cantnfp1  9660  carddomi2  9975  wdomfil  10064  fin1a2lem10  10411  fin1a2lem11  10412  uzsupss  12982  xaddcom  13284  xnegdi  13292  xpncan  13295  xleadd1a  13297  xsubge0  13305  ccat1st1st  14688  swrdccatin1  14786  sgncl  15160  cnpart  15317  fsumcllem  15809  fsumrev2  15859  expcnv  15944  geomulcvg  15956  fprodcllem  16031  fsumdvds  16391  gcd0id  16602  nn0seqcvgd  16653  lcmdvds  16691  mulgcddvds  16738  pcge0  16947  pcneg  16959  pcdvdstr  16961  pcz  16966  pcprmpw2  16967  pcadd  16974  ramcl2  17101  0ramcl  17108  ramub1lem1  17111  ramcl  17114  mrerintcl  17674  mreriincl  17675  mreexexlem4d  17728  mreclatBAD  18644  chnub  18703  psgnunilem1  19594  odmulg  19657  sylow1lem1  19699  pgpfi  19706  odadd1  19949  odadd2  19950  gsumval3  20008  gsumpt  20063  dprdfcntz  20118  dprd2da  20145  ablfac1eulem  20175  pgpfaclem3  20186  ablsimpgfind  20213  abvneg  20966  lssssr  21112  lspsneq  21283  lspdisj2  21288  drngnidl  21414  cnsubrg  21614  riinopn  23102  riincld  23238  neipeltop  23323  hauscmplem  23600  cmpfi  23602  ptbasfi  23775  xkoccn  23813  txindislem  23827  txtube  23834  hmphindis  23991  fclscmp  24224  utop2nei  24444  nrginvrcn  24886  nmoleub  24925  blcvx  24992  xrsxmet  25004  xrsblre  25006  lebnumlem3  25159  cphsqrtcl2  25382  ovollb2  25685  ioorcl  25773  i1fmulc  25899  itg1mulc  25900  mbfi1fseqlem4  25914  bddiblnc  26038  dvlip  26189  dvne0  26207  ig1pdvds  26374  plyeq0lem  26404  plyeq0  26405  aannenlem2  26529  aalioulem6  26537  abelthlem8  26639  abelth  26641  cxpexp  26870  cxpge0  26885  cxpmul2  26891  abscxp2  26895  abscxpbnd  26955  cxpeq  26959  nnlogbexp  26983  isosctrlem2  27021  atanrecl  27113  wilthlem2  27270  dchrabs2  27463  dchr1re  27464  lgsneg1  27523  lgsdirprm  27532  lgsdir  27533  lgsne0  27536  lgsdirnn0  27545  lgsdinn0  27546  2sqlem9  27628  rpvmasumlem  27688  dchrvmasumiflem1  27702  dchrisum0flblem1  27709  rpvmasum2  27713  pntrsumbnd2  27768  pntleml  27812  tgcgrextend  28791  tgbtwnexch2  28802  tgifscgr  28814  tgcolg  28860  tgidinside  28877  tgbtwnconn1lem2  28879  tgbtwnconn1lem3  28880  lnhl  28924  tglinethru  28946  tglineneq  28955  coltr  28958  coltr3  28959  colline  28960  tglnpt2  28963  tglnpt4  28965  mirreu3  28968  miriso  28984  mirln  28990  mirln2  28991  mirconn  28992  mirbtwnhl  28994  colmid  29002  krippenlem  29004  midexlem  29006  ragflat  29021  ragcgr  29024  perprag  29044  perpdragALT  29045  colperpexlem1  29048  colperpexlem3  29050  midex  29055  opphllem1  29065  opphllem2  29066  opphllem5  29069  opphllem6  29070  hlpasch  29075  lnincplng  29103  lnssplng  29111  mirplncl  29114  lmiisolem  29142  hypcgrlem1  29146  hypcgrlem2  29147  cgrg3col4  29207  prlnghpg  29233  perpprlng  29237  prlngmolem2  29240  prlngpln4  29245  prlngplngtr  29246  prlngmid2  29248  upgrex  29479  crctcshwlk  30208  crctcsh  30210  1wlkdlem2  30526  eupth2lem3lem3  30618  eupth2lem3lem7  30622  nmcoplbi  32417  nmophmi  32420  nmbdfnlbi  32438  disjdifprg  32957  imadifxp  32983  2ndimaxp  33028  mptiffisupp  33075  xlt2addrd  33141  ssnnssfz  33169  gsumpart  33414  suppgsumssiun  33423  symgcntz  33436  fzo0pmtrlast  33443  pmtridf1o  33445  pmtridfv1  33446  pmtridfv2  33447  psgnfzto1stlem  33451  tocycf  33468  cycpmco2lem5  33481  cycpmco2  33484  fxpgaval  33518  linds2eq  33725  dvdsruasso  33729  ply1coedeg  33910  ply1degltel  33915  ply1degleel  33916  ig1pmindeg  33923  esplyind  33996  fldext2chn  34149  constraddcl  34183  constrremulcl  34188  constrsqrtcl  34200  cos9thpiminplylem2  34204  locfinref  34262  zarcmplem  34302  esumpr2  34488  unelldsys  34580  sigapildsyslem  34583  sigapildsys  34584  mbfmcst  34681  carsgsigalem  34737  carsgclctunlem3  34742  pmeasmono  34746  probun  34841  0rrv  34873  signsvtn0  34989  signstfvneq0  34991  fineqvac  35553  wevgblacfn  35619  btwnconn1lem11  36610  finxp00  38089  matunitlindf  38310  poimirlem14  38326  mblfinlem1  38349  mblfinlem2  38350  ismblfin  38353  itg2addnclem  38363  itgaddnclem2  38371  areacirclem4  38403  areacirc  38405  isbnd3  38476  blbnd  38479  rrnequiv  38527  lsmsat  39823  lkrscss  39913  eqlkr  39914  lkrshpor  39922  atcvrj2b  40247  atltcvr  40250  3dim1  40282  3dim2  40283  3dim3  40284  ps-2  40293  2at0mat0  40340  dalemdnee  40481  dalem63  40550  lnatexN  40594  2llnma3r  40603  pmodlem1  40661  pmapjat1  40668  pclfinclN  40765  osumclN  40782  pexmidALTN  40793  lhpexle2lem  40824  lhpexle3lem  40826  4atexlemex6  40889  4atex  40891  trlnle  41001  trlval3  41002  cdlemc  41012  cdlemd9  41021  cdleme27N  41184  cdleme28c  41187  cdleme32fvaw  41254  cdleme42ke  41300  cdleme42keg  41301  cdleme42mgN  41303  cdleme17d  41313  cdleme48fvg  41315  cdleme50trn123  41369  cdlemb3  41421  cdlemg8  41446  cdlemg15a  41470  cdlemg15  41471  cdlemg16  41472  cdlemg16ALTN  41473  cdlemg16z  41474  cdlemg16zz  41475  cdlemg20  41500  cdlemg22  41502  cdlemg37  41504  cdlemg31d  41515  cdlemg39  41531  cdlemg40  41532  ltrncom  41553  tendotr  41645  cdlemk25-3  41719  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk53b  41771  cdlemk53  41772  cdlemk55  41776  cdlemk35u  41779  cdlemk55u  41781  cdlemk39u  41783  cdlemk19u  41785  cdleml5N  41795  dia2dimlem7  41885  dia2dimlem13  41891  dih1dimatlem  42144  dihlsprn  42146  dihjat1lem  42243  dihjat1  42244  dvh2dim  42260  dochexmid  42283  lclkrlem1  42321  lclkrlem2i  42330  lclkrlem2t  42341  lcfrlem34  42391  lcfrlem38  42395  lcfrlem41  42398  mapdindp1  42535  mapdindp2  42536  mapdh6dN  42554  mapdh6jN  42560  mapdh8j  42602  mapdh8  42603  hdmap1l6d  42628  hdmap1l6j  42634  hdmap11lem2  42657  hdmap14lem7  42689  primrootlekpowne0  42913  aks6d1c7lem2  42989  unitscyglem4  43006  jm2.19  43761  jm2.23  43764  nzss  45068  disjxp1  45830  cnrefiisplem  46584  xlimliminflimsup  46617  stoweidlem58  46813  fourierdlem41  46903  fourierdlem48  46909  fouriersw  46986  etransclem24  47013  nnfoctbdjlem  47210  smfpimltxr  47502  smfpimgtxr  47535  chnerlem1  47639  sqrtqaa  47647  ssnn0ssfz  49170  mreclat  49816