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  961  euor2  2640  moanimlem  2645  moexexlem  2653  eueq3  3674  opprc1  4855  opprc2  4856  mosubopt  5479  tz6.12-2  6854  nfvres  6905  fvco4i  6969  fvmptex  6990  fvopab4ndm  7006  ressnop0  7136  csbriota  7368  ovprc  7434  ovprc1  7435  ovprc2  7436  ndmovass  7584  ndmovdistr  7585  extmptsuppeq  8168  funsssuppss  8170  eceqoveq  8804  supval2  9401  axpowndlem3  10557  adderpq  10914  mulerpq  10915  fzoval  13665  swrdnznd  14656  pfxnd0  14702  grpidval  18695  tgdif0  23052  resstopn  23246  prcinf  35409  fineqvnttrclselem1  35417  rdgprc0  36141  bj-projval  37481  wl-nax6im  38021  itg2addnclem3  38172  or3or  44599  ndmafv  47734  nfunsnafv  47736  afvnufveq  47741  aovprc  47782  ndmaovass  47800  ndmaovdistr  47801  tz6.12-2-afv2  47831  naryfval  49250  naryfvalixp  49251