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  2613  moanimlem  2618  moexexlem  2626  eueq3  3669  opprc1  4853  opprc2  4854  mosubopt  5458  tz6.12-2  6821  nfvres  6872  fvco4i  6935  fvmptex  6955  fvopab4ndm  6971  ressnop0  7098  csbriota  7330  ovprc  7396  ovprc1  7397  ovprc2  7398  ndmovass  7546  ndmovdistr  7547  extmptsuppeq  8130  funsssuppss  8132  eceqoveq  8759  supval2  9358  axpowndlem3  10510  adderpq  10867  mulerpq  10868  fzoval  13576  swrdnznd  14566  pfxnd0  14612  grpidval  18586  tgdif0  22936  resstopn  23130  prcinf  35269  fineqvnttrclselem1  35277  rdgprc0  35985  bj-projval  37197  wl-nax6im  37723  itg2addnclem3  37874  or3or  44264  ndmafv  47386  nfunsnafv  47388  afvnufveq  47393  aovprc  47434  ndmaovass  47452  ndmaovdistr  47453  tz6.12-2-afv2  47483  naryfval  48874  naryfvalixp  48875