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  949  euor2  2616  moanimlem  2621  moexexlem  2629  eueq3  3733  opprc1  4921  opprc2  4922  mosubopt  5529  nfvres  6961  fvco4i  7023  fvmptex  7043  fvopab4ndm  7059  ressnop0  7187  csbriota  7420  ovprc  7486  ovprc1  7487  ovprc2  7488  ndmovass  7638  ndmovdistr  7639  extmptsuppeq  8229  funsssuppss  8231  eceqoveq  8880  supval2  9524  axpowndlem3  10668  adderpq  11025  mulerpq  11026  fzoval  13717  swrdnznd  14690  pfxnd0  14736  grpidval  18699  tgdif0  23020  resstopn  23215  prcinf  35070  rdgprc0  35757  bj-projval  36962  wl-nax6im  37472  itg2addnclem3  37633  or3or  43985  ndmafv  47055  nfunsnafv  47057  afvnufveq  47062  aovprc  47103  ndmaovass  47121  ndmaovdistr  47122  tz6.12-2-afv2  47152  naryfval  48362  naryfvalixp  48363