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  945  euor2  2615  moanimlem  2620  moexexlem  2628  eueq3  3641  opprc1  4825  opprc2  4826  mosubopt  5418  nfvres  6792  fvco4i  6851  fvmptex  6871  fvopab4ndm  6886  ressnop0  7007  csbriota  7228  ovprc  7293  ovprc1  7294  ovprc2  7295  ndmovass  7438  ndmovdistr  7439  extmptsuppeq  7975  funsssuppss  7977  eceqoveq  8569  supval2  9144  axpowndlem3  10286  adderpq  10643  mulerpq  10644  fzoval  13317  swrdnznd  14283  pfxnd0  14329  grpidval  18260  tgdif0  22050  resstopn  22245  rdgprc0  33675  bj-projval  35113  wl-nax6im  35604  itg2addnclem3  35757  or3or  41520  ndmafv  44519  nfunsnafv  44521  afvnufveq  44526  aovprc  44567  ndmaovass  44585  ndmaovdistr  44586  tz6.12-2-afv2  44616  naryfval  45862  naryfvalixp  45863