Theorem sylc 68

Description: A syllogism inference combined with contraction.

Hypotheses

Ref	Expression
sylc.1	⊢ (φ → (ψ → χ))
sylc.2	⊢ (θ → φ)
sylc.3	⊢ (θ → ψ)

Assertion

Ref	Expression
sylc	⊢ (θ → χ)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.3	. 2 ⊢ (θ → ψ)
2		sylc.2	. . 3 ⊢ (θ → φ)
3		sylc.1	. . 3 ⊢ (φ → (ψ → χ))
4	2, 3	syl 10	. 2 ⊢ (θ → (ψ → χ))
5	1, 4	mpd 26	1 ⊢ (θ → χ)

Syntax hints:   → wi 3

This theorem is referenced by:  pm2.65d 134  jc 136  jaod 424  sylanc 473  sbc5g 1999  sbc6g 2000  tz7.7 3001  reuuniss2 3114  rabsnt 3117  ssorduni 3147  suceloni 3170  unielrel 3619  zfrep6 3721  oprabval3 4090  curry1 4193  curry2 4196  tfrlem13 4224  th3q 4458  f1oen2g 4535  ac6sfi 4591  domnsym 4608  limensuci 4653  unfilem3 4696  supmax 4732  inf3lem7 4764  noinfep 4786  r1val1 4804  imadomg 4952  unidom 4954  ltexpri 5303  prlem936 5309  recexpr 5314  supexpr 5317  lemul12a 5988  lemulge11 5992  nngt0 6091  nnaddm1cl 6104  rpge0 6200  supxrunb1 6257  supxrunb2 6258  nn0ltp1le 6295  nn0ind-raph 6385  qbtwnre 6418  fldiv 6456  eliooord 6514  cardfz 6671  facavg 7158  climubii 7356  cvgcmpi 7388  cvgcmpubi 7389  reccnv 7422  erelem3 7526  efaddlem16 7558  efaddlem25 7567  eftabsi 7580  abspef01tlubi 7603  absefm1lei 7620  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  cos01gt0 7686  efieq1re 7694  ruclem33 7754  ruclem35 7756  metcnp 8098  tgioolem 8125  lmnn 8146  vacnlem3 8584  nmcn3 8595  nmcnc 8596  ubthlem13 8800  ubthlem13OLD 8801  pilem2 8939  pilem3 8940  bcsiALT 9322  hhcms 9348  hlimcauii 9382  hhsscms 9426  projlem26 9487  projlem27 9488  pjthlem10 9504  ococin 9573  spanpr 9779  osumlem2 9857  osumlem4 9859  pjorthi 9892  adjeq 10139  nmbdoplbi 10228  nmcopexlem3 10232  nmcoplbi 10237  nmbdfnlbi 10257  nmcfnexlem3 10261  nmcfnlbi 10266  nmopcoi 10307  branmfn 10317  branmfnOLD 10318  hstnmoc 10431  mdsl0 10518  atomli 10591  atcvat4i 10606  atabsi 10610  infi1 10735  jidd 10840  midd 10841  dupos1 10876  opidon 10898  rnplrnml3 10950  truni1 10999  truni3 11001  hmphsyma 11034  hmphtr 11037  homcard 11045  fgsb2 11086  altretop 11144  cnvtr 11161  rdmob 11202  cmpassoh 11256  homgrf 11257  cmpmon 11270  idmon 11272  immon 11273  idsubfun 11312  fictb 11423  ordiso 11426  ordtypelem6 11432  omsubsuc 11438  omsubsdomlem2 11441  omsubsdom 11442  elomsubsd 11446  omsublim 11448  omsubindss 11449  infenomsub 11450  omsubinit 11451  opncldf2 11455  opncldf3 11456  compcov 11486  alexsublem4 11499  reconnlem1 11507  reconnlem4 11510  reconnlem5 11511  ivthALT 11515  isfne3 11543  fnessref 11564  refssfne 11565  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  filrn 11643  isufil2 11650  ufprim 11654  filssufillem 11655  ufinffr 11663  ufilen 11664  filcon 11665  limfil 11675  limfilcf 11683  flimcls 11684  isfilmap 11689  elfilmap3 11692  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  sflimf 11708  sfcls 11716  filclus 11717  flimfnfcls 11727  sfclusf 11736  tailf 11756  istail 11757  filnetlem5 11767  filnet 11768  ssga 11777  abrexdom 11826  indexd 11846  uptx 11978  heiborlem9 12019  heiborlem14 12024

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain