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  946  euor2  2615  moanimlem  2620  moexexlem  2628  eueq3  3646  opprc1  4828  opprc2  4829  mosubopt  5424  nfvres  6810  fvco4i  6869  fvmptex  6889  fvopab4ndm  6904  ressnop0  7025  csbriota  7248  ovprc  7313  ovprc1  7314  ovprc2  7315  ndmovass  7460  ndmovdistr  7461  extmptsuppeq  8004  funsssuppss  8006  eceqoveq  8611  supval2  9214  axpowndlem3  10355  adderpq  10712  mulerpq  10713  fzoval  13388  swrdnznd  14355  pfxnd0  14401  grpidval  18345  tgdif0  22142  resstopn  22337  rdgprc0  33769  bj-projval  35186  wl-nax6im  35677  itg2addnclem3  35830  or3or  41631  ndmafv  44632  nfunsnafv  44634  afvnufveq  44639  aovprc  44680  ndmaovass  44698  ndmaovdistr  44699  tz6.12-2-afv2  44729  naryfval  45974  naryfvalixp  45975