Theorem sdomdom 8978

Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)

Assertion

Ref	Expression
sdomdom	⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)

Proof of Theorem sdomdom

Step	Hyp	Ref	Expression
1		brsdom 8973	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
2	1	simplbi 496	1 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5147   ≈ cen 8938   ≼ cdom 8939   ≺ csdm 8940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-br 5148  df-sdom 8944

This theorem is referenced by:  domdifsn  9056  sucdom2OLD  9084  sdomnsym  9100  sdomdomtr  9112  domsdomtr  9114  sdomtr  9117  domnsymfi  9205  sdomdomtrfi  9206  domsdomtrfi  9207  sucdom2  9208  php3  9214  1sdom2dom  9249  sucxpdom  9257  findcard3  9287  isfinite2  9303  pwfiOLD  9349  card2on  9551  fict  9650  fidomtri2  9991  prdom2  10003  infxpenlem  10010  indcardi  10038  alephnbtwn2  10069  alephsucdom  10076  alephdom  10078  dfac13  10139  djulepw  10189  infdjuabs  10203  infdif  10206  infunsdom1  10210  infunsdom  10211  infxp  10212  cfslb2n  10265  sdom2en01  10299  isfin32i  10362  fin34  10387  fin67  10392  hsmexlem1  10423  hsmex3  10431  entri3  10556  alephexp1  10576  gchdomtri  10626  canthp1  10651  pwfseqlem5  10660  gchdjuidm  10665  gchxpidm  10666  gchpwdom  10667  hargch  10670  gchaclem  10675  gchhar  10676  gchac  10678  inawinalem  10686  inar1  10772  rankcf  10774  tskuni  10780  grothac  10827  rpnnen  16174  rexpen  16175  aleph1irr  16193  dis1stc  23223  hauspwdom  23225  sibfof  33637  ctbssinf  36590  pibt2  36601  heiborlem3  36984  harinf  42075  saluncl  45331  meadjun  45476  meaiunlelem  45482  omeunle  45530