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  2610  moanimlem  2615  moexexlem  2623  eueq3  3719  opprc1  4901  opprc2  4902  mosubopt  5519  nfvres  6947  fvco4i  7009  fvmptex  7029  fvopab4ndm  7045  ressnop0  7172  csbriota  7402  ovprc  7468  ovprc1  7469  ovprc2  7470  ndmovass  7620  ndmovdistr  7621  extmptsuppeq  8211  funsssuppss  8213  eceqoveq  8860  supval2  9492  axpowndlem3  10636  adderpq  10993  mulerpq  10994  fzoval  13696  swrdnznd  14676  pfxnd0  14722  grpidval  18686  tgdif0  23014  resstopn  23209  prcinf  35086  rdgprc0  35774  bj-projval  36978  wl-nax6im  37498  itg2addnclem3  37659  or3or  44012  ndmafv  47089  nfunsnafv  47091  afvnufveq  47096  aovprc  47137  ndmaovass  47155  ndmaovdistr  47156  tz6.12-2-afv2  47186  naryfval  48477  naryfvalixp  48478