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  34765  bj-projval  35877  wl-nax6im  36387  itg2addnclem3  36541  or3or  42774  ndmafv  45848  nfunsnafv  45850  afvnufveq  45855  aovprc  45896  ndmaovass  45914  ndmaovdistr  45915  tz6.12-2-afv2  45945  naryfval  47314  naryfvalixp  47315