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  44274  ndmafv  47396  nfunsnafv  47398  afvnufveq  47403  aovprc  47444  ndmaovass  47462  ndmaovdistr  47463  tz6.12-2-afv2  47493  naryfval  48884  naryfvalixp  48885