Theorem syl3c 66

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses

Ref	Expression
syl3c.1	⊢ (𝜑 → 𝜓)
syl3c.2	⊢ (𝜑 → 𝜒)
syl3c.3	⊢ (𝜑 → 𝜃)
syl3c.4	⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))

Assertion

Ref	Expression
syl3c	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2 ⊢ (𝜑 → 𝜃)
2		syl3c.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl3c.2	. . 3 ⊢ (𝜑 → 𝜒)
4		syl3c.4	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
5	2, 3, 4	sylc 65	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
6	1, 5	mpd 15	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4

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

This theorem is referenced by:  fodomr  9079  dffi3  9376  cantnflt  9617  cantnflem1  9634  axdc3lem2  10396  seqf1olem2  13958  wrd2ind  14623  relexpindlem  14960  rtrclind  14962  o1fsum  15709  lcmneg  16490  prmind2  16572  rami  16898  ramcl  16912  pslem  18475  telgsums  19784  islbs3  20675  psgndif  21043  mplsubglem  21442  mpllsslem  21443  gsummatr01lem4  22044  lmmo  22768  cnmpt12  23055  cnmpt22  23062  filss  23241  flimopn  23363  flimrest  23371  cfil3i  24670  equivcfil  24700  equivcau  24701  ovolicc2lem3  24920  limciun  25295  dvcnvrelem1  25418  dvfsumrlim  25432  dvfsum2  25435  dgrco  25673  scvxcvx  26372  ftalem3  26461  2sqlem6  26808  2sqlem8  26811  dchrisumlema  26873  dchrisumlem2  26875  addsproplem1  27324  negsproplem1  27369  gropd  28045  grstructd  28046  pthdepisspth  28746  pjoi0  30722  atomli  31387  archirng  32094  archiabllem1a  32097  archiabllem2a  32100  archiabl  32104  crefi  32517  pcmplfin  32530  sigaclcu  32805  measvun  32897  signsply0  33252  bnj1128  33691  bnj1204  33713  bnj1417  33742  neibastop2lem  34908  poimirlem31  36182  ftc1cnnclem  36222  sdclem2  36274  heibor1lem  36341  cvrat4  37979  hdmapval2  40368  ismrcd1  41079  relexpxpmin  42111  ee222  42906  ee333  42911  ee1111  42920  sbcoreleleq  42939  ordelordALT  42941  trsbc  42944  ee110  43081  ee101  43083  ee011  43085  ee100  43087  ee010  43089  ee001  43091  eel11111  43127  fnchoice  43356  fiiuncl  43395  mullimc  43977  islptre  43980  mullimcf  43984  addlimc  44009  stoweidlem20  44381  stoweidlem59  44420  perfectALTVlem2  46034