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  2608  moanimlem  2613  moexexlem  2621  eueq3  3665  opprc1  4846  opprc2  4847  mosubopt  5448  tz6.12-2  6809  nfvres  6860  fvco4i  6923  fvmptex  6943  fvopab4ndm  6959  ressnop0  7086  csbriota  7318  ovprc  7384  ovprc1  7385  ovprc2  7386  ndmovass  7534  ndmovdistr  7535  extmptsuppeq  8118  funsssuppss  8120  eceqoveq  8746  supval2  9339  axpowndlem3  10490  adderpq  10847  mulerpq  10848  fzoval  13560  swrdnznd  14550  pfxnd0  14596  grpidval  18569  tgdif0  22907  resstopn  23101  prcinf  35136  fineqvnttrclselem1  35141  rdgprc0  35835  bj-projval  37040  wl-nax6im  37562  itg2addnclem3  37723  or3or  44126  ndmafv  47250  nfunsnafv  47252  afvnufveq  47257  aovprc  47298  ndmaovass  47316  ndmaovdistr  47317  tz6.12-2-afv2  47347  naryfval  48739  naryfvalixp  48740