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  951  euor2  2613  moanimlem  2618  moexexlem  2626  eueq3  3657  opprc1  4840  opprc2  4841  mosubopt  5464  tz6.12-2  6827  nfvres  6878  fvco4i  6941  fvmptex  6962  fvopab4ndm  6978  ressnop0  7107  csbriota  7339  ovprc  7405  ovprc1  7406  ovprc2  7407  ndmovass  7555  ndmovdistr  7556  extmptsuppeq  8138  funsssuppss  8140  eceqoveq  8769  supval2  9368  axpowndlem3  10522  adderpq  10879  mulerpq  10880  fzoval  13614  swrdnznd  14605  pfxnd0  14651  grpidval  18629  tgdif0  22957  resstopn  23151  prcinf  35257  fineqvnttrclselem1  35265  rdgprc0  35973  bj-projval  37303  wl-nax6im  37843  itg2addnclem3  37994  or3or  44450  ndmafv  47588  nfunsnafv  47590  afvnufveq  47595  aovprc  47636  ndmaovass  47654  ndmaovdistr  47655  tz6.12-2-afv2  47685  naryfval  49104  naryfvalixp  49105