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  3717  opprc1  4897  opprc2  4898  mosubopt  5515  nfvres  6947  fvco4i  7010  fvmptex  7030  fvopab4ndm  7046  ressnop0  7173  csbriota  7403  ovprc  7469  ovprc1  7470  ovprc2  7471  ndmovass  7621  ndmovdistr  7622  extmptsuppeq  8213  funsssuppss  8215  eceqoveq  8862  supval2  9495  axpowndlem3  10639  adderpq  10996  mulerpq  10997  fzoval  13700  swrdnznd  14680  pfxnd0  14726  grpidval  18674  tgdif0  22999  resstopn  23194  prcinf  35108  rdgprc0  35794  bj-projval  36997  wl-nax6im  37519  itg2addnclem3  37680  or3or  44036  ndmafv  47152  nfunsnafv  47154  afvnufveq  47159  aovprc  47200  ndmaovass  47218  ndmaovdistr  47219  tz6.12-2-afv2  47249  naryfval  48549  naryfvalixp  48550