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  3658  opprc1  4841  opprc2  4842  mosubopt  5459  tz6.12-2  6822  nfvres  6873  fvco4i  6936  fvmptex  6957  fvopab4ndm  6973  ressnop0  7101  csbriota  7333  ovprc  7399  ovprc1  7400  ovprc2  7401  ndmovass  7549  ndmovdistr  7550  extmptsuppeq  8132  funsssuppss  8134  eceqoveq  8763  supval2  9362  axpowndlem3  10516  adderpq  10873  mulerpq  10874  fzoval  13608  swrdnznd  14599  pfxnd0  14645  grpidval  18623  tgdif0  22970  resstopn  23164  prcinf  35276  fineqvnttrclselem1  35284  rdgprc0  35992  bj-projval  37322  wl-nax6im  37860  itg2addnclem3  38011  or3or  44471  ndmafv  47603  nfunsnafv  47605  afvnufveq  47610  aovprc  47651  ndmaovass  47669  ndmaovdistr  47670  tz6.12-2-afv2  47700  naryfval  49119  naryfvalixp  49120