Theorem nsyl2 141

Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)

Hypotheses

Ref	Expression
nsyl2.1	⊢ (𝜑 → ¬ 𝜓)
nsyl2.2	⊢ (¬ 𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl2	⊢ (𝜑 → 𝜒)

Proof of Theorem nsyl2

Step	Hyp	Ref	Expression
1		nsyl2.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl2.2	. . 3 ⊢ (¬ 𝜒 → 𝜓)
3	1, 2	nsyl3 138	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 114	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  con1i  147  oprcl  4861  epelg  5543  elfvdm  6884  ovrcl  7403  tfi  7794  limom  7823  oaabs2  8600  ecexr  8660  elpmi  8791  elmapex  8793  pmresg  8815  pmsspw  8822  ixpssmap2g  8872  ixpssmapg  8873  resixpfo  8881  infensuc  9106  pm54.43lem  9945  alephnbtwn  10016  cfpwsdom  10529  elbasfv  17100  elbasov  17101  restsspw  17327  homarcl  17928  isipodrs  18440  grpidval  18530  efgrelexlema  19545  subcmn  19629  dvdsrval  20088  elocv  21109  mvrf1  21431  pf1rcl  21752  matrcl  21796  restrcl  22545  ssrest  22564  iscnp2  22627  isfcls  23397  isnghm  24124  dchrrcl  26625  sltval2  27041  sltres  27047  clwwlknnn  29040  hmdmadj  30945  indispconn  33915  cvmtop1  33941  cvmtop2  33942  mrsub0  34197  mrsubf  34198  mrsubccat  34199  mrsubcn  34200  mrsubco  34202  mrsubvrs  34203  msubf  34213  mclsrcl  34242  dfon2lem7  34450  funpartlem  34603  rankeq1o  34832  bj-brrelex12ALT  35611  bj-fvimacnv0  35830  atbase  37824  llnbase  38045  lplnbase  38070  lvolbase  38114  lhpbase  38534  mapco2g  41095