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  2606  moanimlem  2611  moexexlem  2619  eueq3  3682  opprc1  4861  opprc2  4862  mosubopt  5470  nfvres  6899  fvco4i  6962  fvmptex  6982  fvopab4ndm  6998  ressnop0  7125  csbriota  7359  ovprc  7425  ovprc1  7426  ovprc2  7427  ndmovass  7577  ndmovdistr  7578  extmptsuppeq  8167  funsssuppss  8169  eceqoveq  8795  supval2  9406  axpowndlem3  10552  adderpq  10909  mulerpq  10910  fzoval  13621  swrdnznd  14607  pfxnd0  14653  grpidval  18588  tgdif0  22879  resstopn  23073  prcinf  35084  rdgprc0  35781  bj-projval  36984  wl-nax6im  37506  itg2addnclem3  37667  or3or  44012  ndmafv  47141  nfunsnafv  47143  afvnufveq  47148  aovprc  47189  ndmaovass  47207  ndmaovdistr  47208  tz6.12-2-afv2  47238  naryfval  48617  naryfvalixp  48618