Theorem nsyl5 160

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 159	. 2 ⊢ (¬ 𝜒 → 𝜓)
4	3	con1i 148	1 ⊢ (¬ 𝜓 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm5.55  963  euor2  2641  moanimlem  2646  moexexlem  2654  eueq3  3671  opprc1  4857  opprc2  4858  mosubopt  5485  mosubott  5487  tz6.12-2  6880  nfvres  6931  fvco4i  6995  fvmptex  7016  fvopab4ndm  7032  ressnop0  7165  csbriota  7399  ovprc  7465  ovprc1  7466  ovprc2  7467  ndmovass  7616  ndmovdistr  7617  extmptsuppeq  8216  funsssuppss  8218  eceqoveq  8854  supval2  9457  axpowndlem3  10694  adderpq  11051  mulerpq  11052  fzoval  13804  swrdnznd  14801  pfxnd0  14849  grpidval  18852  tgdif0  23322  resstopn  23516  prcinf  35852  fineqvnttrclselem1  35860  rdgprc0  36682  bj-projval  38036  wl-nax6im  38590  itg2addnclem3  38731  or3or  45163  ndmafv  48349  nfunsnafv  48351  afvnufveq  48356  aovprc  48397  ndmaovass  48415  ndmaovdistr  48416  tz6.12-2-afv2  48446  naryfval  49879  naryfvalixp  49880