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  2607  moanimlem  2612  moexexlem  2620  eueq3  3685  opprc1  4864  opprc2  4865  mosubopt  5473  nfvres  6902  fvco4i  6965  fvmptex  6985  fvopab4ndm  7001  ressnop0  7128  csbriota  7362  ovprc  7428  ovprc1  7429  ovprc2  7430  ndmovass  7580  ndmovdistr  7581  extmptsuppeq  8170  funsssuppss  8172  eceqoveq  8798  supval2  9413  axpowndlem3  10559  adderpq  10916  mulerpq  10917  fzoval  13628  swrdnznd  14614  pfxnd0  14660  grpidval  18595  tgdif0  22886  resstopn  23080  prcinf  35091  rdgprc0  35788  bj-projval  36991  wl-nax6im  37513  itg2addnclem3  37674  or3or  44019  ndmafv  47145  nfunsnafv  47147  afvnufveq  47152  aovprc  47193  ndmaovass  47211  ndmaovdistr  47212  tz6.12-2-afv2  47242  naryfval  48621  naryfvalixp  48622