Theorem nsyl5 162

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 161	. 2 ⊢ (¬ 𝜒 → 𝜓)
4	3	con1i 149	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  946  euor2  2674  moanimlem  2680  moexexlem  2688  eueq3  3650  opprc1  4789  opprc2  4790  mosubopt  5365  nfvres  6681  fvco4i  6739  fvmptex  6759  fvopab4ndm  6774  ressnop0  6892  csbriota  7108  ovprc  7173  ovprc1  7174  ovprc2  7175  ndmovass  7316  ndmovdistr  7317  extmptsuppeq  7837  funsssuppss  7839  eceqoveq  8385  supval2  8903  axpowndlem3  10010  adderpq  10367  mulerpq  10368  fzoval  13034  swrdnznd  13995  pfxnd0  14041  grpidval  17863  tgdif0  21597  resstopn  21791  rdgprc0  33151  bj-projval  34432  wl-nax6im  34923  itg2addnclem3  35110  or3or  40724  ndmafv  43696  nfunsnafv  43698  afvnufveq  43703  aovprc  43744  ndmaovass  43762  ndmaovdistr  43763  tz6.12-2-afv2  43793  naryfval  45042  naryfvalixp  45043