Theorem nsyl2 142

Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)

Hypotheses

Ref	Expression
nsyl2.1	⊢ (𝜑 → ¬ 𝜓)
nsyl2.2	⊢ (¬ 𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl2	⊢ (𝜑 → 𝜒)

Proof of Theorem nsyl2

Step	Hyp	Ref	Expression
1		nsyl2.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl2.2	. . 3 ⊢ (¬ 𝜒 → 𝜓)
3	1, 2	nsyl3 139	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 115	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con1i  148  oprcl  4859  epelg  5552  elfvdm  6917  ovrcl  7459  elfvov1  7460  elfvov2  7461  tfi  7862  limom  7891  oaabs2  8651  ecexr  8715  elpmi  8859  elmapex  8861  pmresg  8891  pmsspw  8898  ixpssmap2g  8948  ixpssmapg  8949  resixpfo  8957  infensuc  9167  pm54.43lem  10074  alephnbtwn  10143  cfpwsdom  10662  elbasfv  17386  elbasov  17387  restsspw  17595  homarcl  18196  isipodrs  18704  grpidval  18833  efgrelexlema  19956  subcmn  20044  dvdsrval  20584  elocv  21967  mvrf1  22286  pf1rcl  22660  matrcl  22720  restrcl  23468  ssrest  23487  iscnp2  23550  isfcls  24321  isnghm  25035  dchrrcl  27560  ltsval2  28006  ltsres  28012  clwwlknnn  30617  hmdmadj  32535  indispconn  35978  cvmtop1  36004  cvmtop2  36005  mrsub0  36260  mrsubf  36261  mrsubccat  36262  mrsubcn  36263  mrsubco  36265  mrsubvrs  36266  msubf  36276  mclsrcl  36305  dfon2lem7  36531  funpartlem  36686  rankeq1o  36912  bj-brrelex12ALT  37962  bj-fvimacnv0  38187  atbase  40326  llnbase  40546  lplnbase  40571  lvolbase  40615  lhpbase  41035  mapco2g  43704