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  3679  opprc1  4857  opprc2  4858  mosubopt  5465  nfvres  6881  fvco4i  6944  fvmptex  6964  fvopab4ndm  6980  ressnop0  7107  csbriota  7341  ovprc  7407  ovprc1  7408  ovprc2  7409  ndmovass  7557  ndmovdistr  7558  extmptsuppeq  8144  funsssuppss  8146  eceqoveq  8772  supval2  9382  axpowndlem3  10528  adderpq  10885  mulerpq  10886  fzoval  13597  swrdnznd  14583  pfxnd0  14629  grpidval  18570  tgdif0  22912  resstopn  23106  prcinf  35077  rdgprc0  35774  bj-projval  36977  wl-nax6im  37499  itg2addnclem3  37660  or3or  44005  ndmafv  47134  nfunsnafv  47136  afvnufveq  47141  aovprc  47182  ndmaovass  47200  ndmaovdistr  47201  tz6.12-2-afv2  47231  naryfval  48610  naryfvalixp  48611