Theorem nsyl5 159

Description: A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.)

Hypotheses

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

Assertion

Ref	Expression
nsyl5	⊢ (¬ 𝜓 → 𝜒)

Proof of Theorem nsyl5

Step	Hyp	Ref	Expression
1		nsyl4.1	. . 3 ⊢ (𝜑 → 𝜓)
2		nsyl4.2	. . 3 ⊢ (¬ 𝜑 → 𝜒)
3	1, 2	nsyl4 158	. 2 ⊢ (¬ 𝜒 → 𝜓)
4	3	con1i 147	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:  pm5.55  948  euor2  2610  moanimlem  2615  moexexlem  2623  eueq3  3708  opprc1  4898  opprc2  4899  mosubopt  5511  nfvres  6933  fvco4i  6993  fvmptex  7013  fvopab4ndm  7028  ressnop0  7151  csbriota  7381  ovprc  7447  ovprc1  7448  ovprc2  7449  ndmovass  7595  ndmovdistr  7596  extmptsuppeq  8173  funsssuppss  8175  eceqoveq  8816  supval2  9450  axpowndlem3  10594  adderpq  10951  mulerpq  10952  fzoval  13633  swrdnznd  14592  pfxnd0  14638  grpidval  18580  tgdif0  22495  resstopn  22690  rdgprc0  34796  bj-projval  35925  wl-nax6im  36435  itg2addnclem3  36589  or3or  42822  ndmafv  45896  nfunsnafv  45898  afvnufveq  45903  aovprc  45944  ndmaovass  45962  ndmaovdistr  45963  tz6.12-2-afv2  45993  naryfval  47362  naryfvalixp  47363