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  956  euor2  2617  moanimlem  2622  moexexlem  2630  eueq3  3652  opprc1  4828  opprc2  4829  mosubopt  5451  tz6.12-2  6814  nfvres  6865  fvco4i  6929  fvmptex  6950  fvopab4ndm  6966  ressnop0  7096  csbriota  7328  ovprc  7394  ovprc1  7395  ovprc2  7396  ndmovass  7544  ndmovdistr  7545  extmptsuppeq  8128  funsssuppss  8130  eceqoveq  8759  supval2  9358  axpowndlem3  10513  adderpq  10870  mulerpq  10871  fzoval  13605  swrdnznd  14596  pfxnd0  14642  grpidval  18620  tgdif0  22975  resstopn  23169  prcinf  35294  fineqvnttrclselem1  35302  rdgprc0  36019  bj-projval  37349  wl-nax6im  37889  itg2addnclem3  38040  or3or  44467  ndmafv  47603  nfunsnafv  47605  afvnufveq  47610  aovprc  47651  ndmaovass  47669  ndmaovdistr  47670  tz6.12-2-afv2  47700  naryfval  49119  naryfvalixp  49120