Theorem pm2.61dane 3072

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 3071	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ≠ wne 2984

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 2985

This theorem is referenced by:  pm2.61da2ne  3073  pm2.61da3ne  3074  pm2.61iine  3075  disjxiun  4959  onfr  6105  f1oprswap  6526  soex  7482  riiner  8220  difsnen  8446  mapdom2  8535  nnunifi  8615  fofinf1o  8645  brwdom2  8883  cantnff  8983  cantnfp1  8990  carddomi2  9245  wdomfil  9333  fin1a2lem10  9677  fin1a2lem11  9678  uzsupss  12189  xaddcom  12483  xnegdi  12491  xpncan  12494  xleadd1a  12496  xsubge0  12504  cnpart  14433  fsumcllem  14922  fsumrev2  14970  expcnv  15052  geomulcvg  15065  fprodcllem  15138  fsumdvds  15491  gcd0id  15700  nn0seqcvgd  15743  lcmdvds  15781  mulgcddvds  15828  pcge0  16027  pcneg  16039  pcdvdstr  16041  pcz  16046  pcprmpw2  16047  pcadd  16054  ramcl2  16181  0ramcl  16188  ramub1lem1  16191  ramcl  16194  mrerintcl  16697  mreriincl  16698  mreexexlem4d  16747  mreclatBAD  17626  psgnunilem1  18352  odmulg  18413  sylow1lem1  18453  pgpfi  18460  odadd1  18691  odadd2  18692  gsumval3  18748  gsumpt  18802  dprdfcntz  18854  dprd2da  18881  ablfac1eulem  18911  pgpfaclem3  18922  abvneg  19295  lssssr  19415  lspsneq  19584  lspdisj2  19589  drngnidl  19691  cnsubrg  20287  riinopn  21200  riincld  21336  neipeltop  21421  hauscmplem  21698  cmpfi  21700  ptbasfi  21873  xkoccn  21911  txindislem  21925  txtube  21932  hmphindis  22089  fclscmp  22322  utop2nei  22542  nrginvrcn  22984  nmoleub  23023  blcvx  23089  xrsxmet  23100  xrsblre  23102  lebnumlem3  23250  cphsqrtcl2  23473  ovollb2  23773  ioorcl  23861  i1fmulc  23987  itg1mulc  23988  mbfi1fseqlem4  24002  dvlip  24273  dvne0  24291  ig1pdvds  24453  plyeq0lem  24483  plyeq0  24484  aannenlem2  24601  aalioulem6  24609  abelthlem8  24710  abelth  24712  cxpexp  24932  cxpge0  24947  cxpmul2  24953  abscxp2  24957  abscxpbnd  25015  cxpeq  25019  nnlogbexp  25040  isosctrlem2  25078  atanrecl  25170  wilthlem2  25328  dchrabs2  25520  dchr1re  25521  lgsneg1  25580  lgsdirprm  25589  lgsdir  25590  lgsne0  25593  lgsdirnn0  25602  lgsdinn0  25603  2sqlem9  25685  rpvmasumlem  25745  dchrvmasumiflem1  25759  dchrisum0flblem1  25766  rpvmasum2  25770  pntrsumbnd2  25825  pntleml  25869  tgcgrextend  25953  tgbtwnexch2  25964  tgifscgr  25976  tgcolg  26022  tgidinside  26039  tgbtwnconn1lem2  26041  tgbtwnconn1lem3  26042  lnhl  26083  tglinethru  26104  tglnpt2  26109  tglineneq  26112  coltr  26115  coltr3  26116  colline  26117  mirreu3  26122  miriso  26138  mirln  26144  mirln2  26145  mirconn  26146  mirbtwnhl  26148  colmid  26156  krippenlem  26158  midexlem  26160  ragflat  26172  ragcgr  26175  perprag  26194  perpdragALT  26195  colperpexlem1  26198  colperpexlem3  26200  midex  26205  opphllem1  26215  opphllem2  26216  opphllem5  26219  opphllem6  26220  hlpasch  26224  lmiisolem  26264  hypcgrlem1  26267  hypcgrlem2  26268  cgrg3col4  26322  upgrex  26560  crctcshwlk  27287  crctcsh  27289  1wlkdlem2  27604  eupth2lem3lem3  27697  eupth2lem3lem7  27701  nmcoplbi  29496  nmophmi  29499  nmbdfnlbi  29517  disjdifprg  30015  imadifxp  30041  xlt2addrd  30170  ssnnssfz  30198  symgcntz  30388  tocycf  30406  linds2eq  30587  psgnfzto1stlem  30664  pmtridf1o  30670  pmtridfv1  30671  pmtridfv2  30672  locfinref  30722  esumpr2  30943  unelldsys  31034  sigapildsyslem  31037  sigapildsys  31038  mbfmcst  31134  carsgsigalem  31190  carsgclctunlem3  31195  pmeasmono  31199  probun  31294  0rrv  31326  sgncl  31413  signsvtn0  31457  signstfvneq0  31459  btwnconn1lem11  33167  finxp00  34214  matunitlindf  34421  poimirlem14  34437  mblfinlem1  34460  mblfinlem2  34461  ismblfin  34464  itg2addnclem  34474  itgaddnclem2  34482  bddiblnc  34493  areacirclem4  34516  areacirc  34518  isbnd3  34594  blbnd  34597  rrnequiv  34645  lsmsat  35675  lkrscss  35765  eqlkr  35766  lkrshpor  35774  atcvrj2b  36099  atltcvr  36102  3dim1  36134  3dim2  36135  3dim3  36136  ps-2  36145  2at0mat0  36192  dalemdnee  36333  dalem63  36402  lnatexN  36446  2llnma3r  36455  pmodlem1  36513  pmapjat1  36520  pclfinclN  36617  osumclN  36634  pexmidALTN  36645  lhpexle2lem  36676  lhpexle3lem  36678  4atexlemex6  36741  4atex  36743  trlnle  36853  trlval3  36854  cdlemc  36864  cdlemd9  36873  cdleme27N  37036  cdleme28c  37039  cdleme32fvaw  37106  cdleme42ke  37152  cdleme42keg  37153  cdleme42mgN  37155  cdleme17d  37165  cdleme48fvg  37167  cdleme50trn123  37221  cdlemb3  37273  cdlemg8  37298  cdlemg15a  37322  cdlemg15  37323  cdlemg16  37324  cdlemg16ALTN  37325  cdlemg16z  37326  cdlemg16zz  37327  cdlemg20  37352  cdlemg22  37354  cdlemg37  37356  cdlemg31d  37367  cdlemg39  37383  cdlemg40  37384  ltrncom  37405  tendotr  37497  cdlemk25-3  37571  cdlemk35s-id  37605  cdlemk39s-id  37607  cdlemk53b  37623  cdlemk53  37624  cdlemk55  37628  cdlemk35u  37631  cdlemk55u  37633  cdlemk39u  37635  cdlemk19u  37637  cdleml5N  37647  dia2dimlem7  37737  dia2dimlem13  37743  dih1dimatlem  37996  dihlsprn  37998  dihjat1lem  38095  dihjat1  38096  dvh2dim  38112  dochexmid  38135  lclkrlem1  38173  lclkrlem2i  38182  lclkrlem2t  38193  lcfrlem34  38243  lcfrlem38  38247  lcfrlem41  38250  mapdindp1  38387  mapdindp2  38388  mapdh6dN  38406  mapdh6jN  38412  mapdh8j  38454  mapdh8  38455  hdmap1l6d  38480  hdmap1l6j  38486  hdmap11lem2  38509  hdmap14lem7  38541  jm2.19  39075  jm2.23  39078  ablsimpgfind  40167  nzss  40187  disjxp1  40870  cnrefiisplem  41652  xlimliminflimsup  41685  stoweidlem58  41885  fourierdlem41  41975  fourierdlem48  41981  fouriersw  42058  etransclem24  42085  nnfoctbdjlem  42279  ssnn0ssfz  43875