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  950  euor2  2611  moanimlem  2616  moexexlem  2624  eueq3  3667  opprc1  4851  opprc2  4852  mosubopt  5456  tz6.12-2  6819  nfvres  6870  fvco4i  6933  fvmptex  6953  fvopab4ndm  6969  ressnop0  7096  csbriota  7328  ovprc  7394  ovprc1  7395  ovprc2  7396  ndmovass  7544  ndmovdistr  7545  extmptsuppeq  8128  funsssuppss  8130  eceqoveq  8757  supval2  9356  axpowndlem3  10508  adderpq  10865  mulerpq  10866  fzoval  13574  swrdnznd  14564  pfxnd0  14610  grpidval  18584  tgdif0  22934  resstopn  23128  prcinf  35218  fineqvnttrclselem1  35226  rdgprc0  35934  bj-projval  37140  wl-nax6im  37662  itg2addnclem3  37813  or3or  44206  ndmafv  47328  nfunsnafv  47330  afvnufveq  47335  aovprc  47376  ndmaovass  47394  ndmaovdistr  47395  tz6.12-2-afv2  47425  naryfval  48816  naryfvalixp  48817