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  9068  dffi3  9346  cantnflt  9593  cantnflem1  9610  axdc3lem2  10373  seqf1olem2  13977  wrd2ind  14658  relexpindlem  14998  rtrclind  15000  o1fsum  15748  lcmneg  16542  prmind2  16624  rami  16955  ramcl  16969  pslem  18507  telgsums  19934  islbs3  21122  psgndif  21569  mplsubglem  21966  mpllsslem  21967  gsummatr01lem4  22614  lmmo  23336  cnmpt12  23623  cnmpt22  23630  filss  23809  flimopn  23931  flimrest  23939  cfil3i  25237  equivcfil  25267  equivcau  25268  ovolicc2lem3  25488  limciun  25863  dvcnvrelem1  25990  dvfsumrlim  26006  dvfsum2  26009  dgrco  26249  scvxcvx  26964  ftalem3  27053  2sqlem6  27402  2sqlem8  27405  dchrisumlema  27467  dchrisumlem2  27469  addsproplem1  27977  negsproplem1  28036  gropd  29116  grstructd  29117  pthdepisspth  29820  pjoi0  31804  atomli  32469  archirng  33281  archiabllem1a  33284  archiabllem2a  33287  archiabl  33291  crefi  34024  pcmplfin  34037  sigaclcu  34294  measvun  34386  signsply0  34728  bnj1128  35165  bnj1204  35187  bnj1417  35216  neibastop2lem  36573  poimirlem31  37896  ftc1cnnclem  37936  sdclem2  37987  heibor1lem  38054  cvrat4  39813  hdmapval2  42202  ismrcd1  43049  relexpxpmin  44067  ee222  44852  ee333  44857  ee1111  44866  sbcoreleleq  44885  ordelordALT  44887  trsbc  44890  ee110  45027  ee101  45029  ee011  45031  ee100  45033  ee010  45035  ee001  45037  eel11111  45072  fnchoice  45383  fiiuncl  45419  mullimc  45970  islptre  45973  mullimcf  45977  addlimc  46000  stoweidlem20  46372  stoweidlem59  46411  perfectALTVlem2  48076