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  2612  moanimlem  2617  moexexlem  2625  eueq3  3694  opprc1  4873  opprc2  4874  mosubopt  5485  nfvres  6917  fvco4i  6980  fvmptex  7000  fvopab4ndm  7016  ressnop0  7143  csbriota  7377  ovprc  7443  ovprc1  7444  ovprc2  7445  ndmovass  7595  ndmovdistr  7596  extmptsuppeq  8187  funsssuppss  8189  eceqoveq  8836  supval2  9467  axpowndlem3  10613  adderpq  10970  mulerpq  10971  fzoval  13677  swrdnznd  14660  pfxnd0  14706  grpidval  18639  tgdif0  22930  resstopn  23124  prcinf  35125  rdgprc0  35811  bj-projval  37014  wl-nax6im  37536  itg2addnclem3  37697  or3or  44047  ndmafv  47169  nfunsnafv  47171  afvnufveq  47176  aovprc  47217  ndmaovass  47235  ndmaovdistr  47236  tz6.12-2-afv2  47266  naryfval  48608  naryfvalixp  48609