Theorem pm2.61dane 3022

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ≠ wne 2935

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 208  df-an 397  df-ne 2936

This theorem is referenced by:  pm2.61da2ne  3023  pm2.61da3ne  3024  pm2.61iine  3025  disjxiun  5076  onfr  6356  f1oprswap  6819  soex  7868  frxp2  8091  frxp3  8098  riiner  8734  difsnen  8994  mapdom2  9083  nnunifi  9198  fofinf1o  9239  brwdom2  9485  cantnff  9593  cantnfp1  9600  carddomi2  9892  wdomfil  9981  fin1a2lem10  10329  fin1a2lem11  10330  uzsupss  12888  xaddcom  13190  xnegdi  13198  xpncan  13201  xleadd1a  13203  xsubge0  13211  ccat1st1st  14589  swrdccatin1  14685  cnpart  15200  fsumcllem  15692  fsumrev2  15742  expcnv  15827  geomulcvg  15839  fprodcllem  15914  fsumdvds  16275  gcd0id  16486  nn0seqcvgd  16537  lcmdvds  16575  mulgcddvds  16622  pcge0  16831  pcneg  16843  pcdvdstr  16845  pcz  16850  pcprmpw2  16851  pcadd  16858  ramcl2  16985  0ramcl  16992  ramub1lem1  16995  ramcl  16998  mrerintcl  17557  mreriincl  17558  mreexexlem4d  17611  mreclatBAD  18527  chnub  18586  psgnunilem1  19466  odmulg  19529  sylow1lem1  19571  pgpfi  19578  odadd1  19821  odadd2  19822  gsumval3  19880  gsumpt  19935  dprdfcntz  19990  dprd2da  20017  ablfac1eulem  20047  pgpfaclem3  20058  ablsimpgfind  20085  abvneg  20805  lssssr  20951  lspsneq  21122  lspdisj2  21127  drngnidl  21243  cnsubrg  21409  riinopn  22898  riincld  23034  neipeltop  23119  hauscmplem  23396  cmpfi  23398  ptbasfi  23571  xkoccn  23609  txindislem  23623  txtube  23630  hmphindis  23787  fclscmp  24020  utop2nei  24240  nrginvrcn  24682  nmoleub  24721  blcvx  24788  xrsxmet  24800  xrsblre  24802  lebnumlem3  24955  cphsqrtcl2  25178  ovollb2  25481  ioorcl  25569  i1fmulc  25695  itg1mulc  25696  mbfi1fseqlem4  25710  bddiblnc  25834  dvlip  25985  dvne0  26003  ig1pdvds  26170  plyeq0lem  26200  plyeq0  26201  aannenlem2  26320  aalioulem6  26328  abelthlem8  26429  abelth  26431  cxpexp  26657  cxpge0  26672  cxpmul2  26678  abscxp2  26682  abscxpbnd  26742  cxpeq  26746  nnlogbexp  26770  isosctrlem2  26808  atanrecl  26900  wilthlem2  27057  dchrabs2  27250  dchr1re  27251  lgsneg1  27310  lgsdirprm  27319  lgsdir  27320  lgsne0  27323  lgsdirnn0  27332  lgsdinn0  27333  2sqlem9  27415  rpvmasumlem  27475  dchrvmasumiflem1  27489  dchrisum0flblem1  27496  rpvmasum2  27500  pntrsumbnd2  27555  pntleml  27599  tgcgrextend  28578  tgbtwnexch2  28589  tgifscgr  28601  tgcolg  28647  tgidinside  28664  tgbtwnconn1lem2  28666  tgbtwnconn1lem3  28667  lnhl  28708  tglinethru  28729  tglnpt2  28734  tglineneq  28737  coltr  28740  coltr3  28741  colline  28742  mirreu3  28747  miriso  28763  mirln  28769  mirln2  28770  mirconn  28771  mirbtwnhl  28773  colmid  28781  krippenlem  28783  midexlem  28785  ragflat  28797  ragcgr  28800  perprag  28819  perpdragALT  28820  colperpexlem1  28823  colperpexlem3  28825  midex  28830  opphllem1  28840  opphllem2  28841  opphllem5  28844  opphllem6  28845  hlpasch  28849  lmiisolem  28889  hypcgrlem1  28892  hypcgrlem2  28893  cgrg3col4  28946  upgrex  29186  crctcshwlk  29915  crctcsh  29917  1wlkdlem2  30233  eupth2lem3lem3  30325  eupth2lem3lem7  30329  nmcoplbi  32124  nmophmi  32127  nmbdfnlbi  32145  disjdifprg  32671  imadifxp  32697  2ndimaxp  32745  mptiffisupp  32792  xlt2addrd  32858  ssnnssfz  32886  sgncl  32930  gsumpart  33151  suppgsumssiun  33160  symgcntz  33173  fzo0pmtrlast  33180  pmtridf1o  33182  pmtridfv1  33183  pmtridfv2  33184  psgnfzto1stlem  33188  tocycf  33205  cycpmco2lem5  33218  cycpmco2  33221  fxpgaval  33255  linds2eq  33471  dvdsruasso  33475  ply1coedeg  33679  ply1degltel  33684  ply1degleel  33685  ig1pmindeg  33692  esplyind  33766  fldext2chn  33919  constraddcl  33953  constrremulcl  33958  constrsqrtcl  33970  cos9thpiminplylem2  33974  locfinref  34032  zarcmplem  34072  esumpr2  34258  unelldsys  34349  sigapildsyslem  34352  sigapildsys  34353  mbfmcst  34450  carsgsigalem  34506  carsgclctunlem3  34511  pmeasmono  34515  probun  34610  0rrv  34642  signsvtn0  34761  signstfvneq0  34763  fineqvac  35304  wevgblacfn  35344  btwnconn1lem11  36332  finxp00  37771  matunitlindf  37992  poimirlem14  38008  mblfinlem1  38031  mblfinlem2  38032  ismblfin  38035  itg2addnclem  38045  itgaddnclem2  38053  areacirclem4  38085  areacirc  38087  isbnd3  38158  blbnd  38161  rrnequiv  38209  lsmsat  39507  lkrscss  39597  eqlkr  39598  lkrshpor  39606  atcvrj2b  39931  atltcvr  39934  3dim1  39966  3dim2  39967  3dim3  39968  ps-2  39977  2at0mat0  40024  dalemdnee  40165  dalem63  40234  lnatexN  40278  2llnma3r  40287  pmodlem1  40345  pmapjat1  40352  pclfinclN  40449  osumclN  40466  pexmidALTN  40477  lhpexle2lem  40508  lhpexle3lem  40510  4atexlemex6  40573  4atex  40575  trlnle  40685  trlval3  40686  cdlemc  40696  cdlemd9  40705  cdleme27N  40868  cdleme28c  40871  cdleme32fvaw  40938  cdleme42ke  40984  cdleme42keg  40985  cdleme42mgN  40987  cdleme17d  40997  cdleme48fvg  40999  cdleme50trn123  41053  cdlemb3  41105  cdlemg8  41130  cdlemg15a  41154  cdlemg15  41155  cdlemg16  41156  cdlemg16ALTN  41157  cdlemg16z  41158  cdlemg16zz  41159  cdlemg20  41184  cdlemg22  41186  cdlemg37  41188  cdlemg31d  41199  cdlemg39  41215  cdlemg40  41216  ltrncom  41237  tendotr  41329  cdlemk25-3  41403  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk53b  41455  cdlemk53  41456  cdlemk55  41460  cdlemk35u  41463  cdlemk55u  41465  cdlemk39u  41467  cdlemk19u  41469  cdleml5N  41479  dia2dimlem7  41569  dia2dimlem13  41575  dih1dimatlem  41828  dihlsprn  41830  dihjat1lem  41927  dihjat1  41928  dvh2dim  41944  dochexmid  41967  lclkrlem1  42005  lclkrlem2i  42014  lclkrlem2t  42025  lcfrlem34  42075  lcfrlem38  42079  lcfrlem41  42082  mapdindp1  42219  mapdindp2  42220  mapdh6dN  42238  mapdh6jN  42244  mapdh8j  42286  mapdh8  42287  hdmap1l6d  42312  hdmap1l6j  42318  hdmap11lem2  42341  hdmap14lem7  42373  primrootlekpowne0  42597  aks6d1c7lem2  42673  unitscyglem4  42690  jm2.19  43445  jm2.23  43448  nzss  44768  disjxp1  45524  cnrefiisplem  46279  xlimliminflimsup  46312  stoweidlem58  46508  fourierdlem41  46598  fourierdlem48  46604  fouriersw  46681  etransclem24  46708  nnfoctbdjlem  46905  smfpimltxr  47197  smfpimgtxr  47230  chnerlem1  47334  ssnn0ssfz  48847  mreclat  49494