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  951  euor2  2614  moanimlem  2619  moexexlem  2627  eueq3  3671  opprc1  4855  opprc2  4856  mosubopt  5466  tz6.12-2  6829  nfvres  6880  fvco4i  6943  fvmptex  6964  fvopab4ndm  6980  ressnop0  7108  csbriota  7340  ovprc  7406  ovprc1  7407  ovprc2  7408  ndmovass  7556  ndmovdistr  7557  extmptsuppeq  8140  funsssuppss  8142  eceqoveq  8771  supval2  9370  axpowndlem3  10522  adderpq  10879  mulerpq  10880  fzoval  13588  swrdnznd  14578  pfxnd0  14624  grpidval  18598  tgdif0  22948  resstopn  23142  prcinf  35291  fineqvnttrclselem1  35299  rdgprc0  36007  bj-projval  37244  wl-nax6im  37773  itg2addnclem3  37924  or3or  44379  ndmafv  47500  nfunsnafv  47502  afvnufveq  47507  aovprc  47548  ndmaovass  47566  ndmaovdistr  47567  tz6.12-2-afv2  47597  naryfval  48988  naryfvalixp  48989