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  3671  opprc1  4848  opprc2  4849  mosubopt  5453  nfvres  6861  fvco4i  6924  fvmptex  6944  fvopab4ndm  6960  ressnop0  7087  csbriota  7321  ovprc  7387  ovprc1  7388  ovprc2  7389  ndmovass  7537  ndmovdistr  7538  extmptsuppeq  8121  funsssuppss  8123  eceqoveq  8749  supval2  9345  axpowndlem3  10493  adderpq  10850  mulerpq  10851  fzoval  13563  swrdnznd  14549  pfxnd0  14595  grpidval  18535  tgdif0  22877  resstopn  23071  prcinf  35075  fineqvnttrclselem1  35080  rdgprc0  35777  bj-projval  36980  wl-nax6im  37502  itg2addnclem3  37663  or3or  44006  ndmafv  47134  nfunsnafv  47136  afvnufveq  47141  aovprc  47182  ndmaovass  47200  ndmaovdistr  47201  tz6.12-2-afv2  47231  naryfval  48623  naryfvalixp  48624