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  947  euor2  2609  moanimlem  2614  moexexlem  2622  eueq3  3706  opprc1  4896  opprc2  4897  mosubopt  5509  nfvres  6929  fvco4i  6989  fvmptex  7009  fvopab4ndm  7024  ressnop0  7147  csbriota  7377  ovprc  7443  ovprc1  7444  ovprc2  7445  ndmovass  7591  ndmovdistr  7592  extmptsuppeq  8169  funsssuppss  8171  eceqoveq  8812  supval2  9446  axpowndlem3  10590  adderpq  10947  mulerpq  10948  fzoval  13629  swrdnznd  14588  pfxnd0  14634  grpidval  18576  tgdif0  22486  resstopn  22681  rdgprc0  34753  bj-projval  35865  wl-nax6im  36375  itg2addnclem3  36529  or3or  42759  ndmafv  45834  nfunsnafv  45836  afvnufveq  45841  aovprc  45882  ndmaovass  45900  ndmaovdistr  45901  tz6.12-2-afv2  45931  naryfval  47267  naryfvalixp  47268