Theorem nsyl2 142

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 139	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 115	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con1i  148  oprcl  4866  epelg  5564  elfvdm  6919  ovrcl  7457  elfvov1  7458  elfvov2  7459  tfi  7851  limom  7880  oaabs2  8637  ecexr  8701  elpmi  8845  elmapex  8847  pmresg  8870  pmsspw  8877  ixpssmap2g  8927  ixpssmapg  8928  resixpfo  8936  infensuc  9146  pm54.43lem  9998  alephnbtwn  10067  cfpwsdom  10580  elbasfv  17292  elbasov  17293  restsspw  17501  homarcl  18102  isipodrs  18610  grpidval  18736  efgrelexlema  19842  subcmn  19930  dvdsrval  20468  elocv  21847  mvrf1  22164  pf1rcl  22538  matrcl  22598  restrcl  23343  ssrest  23362  iscnp2  23425  isfcls  24195  isnghm  24909  dchrrcl  27433  ltsval2  27849  ltsres  27855  clwwlknnn  30413  hmdmadj  32321  indispconn  35739  cvmtop1  35765  cvmtop2  35766  mrsub0  36021  mrsubf  36022  mrsubccat  36023  mrsubcn  36024  mrsubco  36026  mrsubvrs  36027  msubf  36037  mclsrcl  36066  dfon2lem7  36292  funpartlem  36447  rankeq1o  36676  bj-brrelex12ALT  37736  bj-fvimacnv0  37963  atbase  40096  llnbase  40316  lplnbase  40341  lvolbase  40385  lhpbase  40805  mapco2g  43478