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  4859  epelg  5556  elfvdm  6912  ovrcl  7454  elfvov1  7455  elfvov2  7456  tfi  7849  limom  7878  oaabs2  8637  ecexr  8701  elpmi  8845  elmapex  8847  pmresg  8877  pmsspw  8884  ixpssmap2g  8934  ixpssmapg  8935  resixpfo  8943  infensuc  9153  pm54.43lem  10005  alephnbtwn  10074  cfpwsdom  10593  elbasfv  17307  elbasov  17308  restsspw  17516  homarcl  18117  isipodrs  18625  grpidval  18754  efgrelexlema  19876  subcmn  19964  dvdsrval  20502  elocv  21881  mvrf1  22200  pf1rcl  22574  matrcl  22634  restrcl  23382  ssrest  23401  iscnp2  23464  isfcls  24235  isnghm  24949  dchrrcl  27476  ltsval2  27892  ltsres  27898  clwwlknnn  30503  hmdmadj  32421  indispconn  35813  cvmtop1  35839  cvmtop2  35840  mrsub0  36095  mrsubf  36096  mrsubccat  36097  mrsubcn  36098  mrsubco  36100  mrsubvrs  36101  msubf  36111  mclsrcl  36140  dfon2lem7  36366  funpartlem  36521  rankeq1o  36751  bj-brrelex12ALT  37811  bj-fvimacnv0  38038  atbase  40162  llnbase  40382  lplnbase  40407  lvolbase  40451  lhpbase  40871  mapco2g  43559