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  9063  dffi3  9341  cantnflt  9591  cantnflem1  9608  axdc3lem2  10371  seqf1olem2  14002  wrd2ind  14683  relexpindlem  15023  rtrclind  15025  o1fsum  15774  lcmneg  16570  prmind2  16652  rami  16984  ramcl  16998  pslem  18536  telgsums  19966  islbs3  21155  psgndif  21584  mplsubglem  21980  mpllsslem  21981  gsummatr01lem4  22648  lmmo  23370  cnmpt12  23657  cnmpt22  23664  filss  23843  flimopn  23965  flimrest  23973  cfil3i  25261  equivcfil  25291  equivcau  25292  ovolicc2lem3  25511  limciun  25886  dvcnvrelem1  26009  dvfsumrlim  26023  dvfsum2  26026  dgrco  26265  scvxcvx  26974  ftalem3  27063  2sqlem6  27411  2sqlem8  27414  dchrisumlema  27476  dchrisumlem2  27478  addsproplem1  27986  negsproplem1  28045  gropd  29125  grstructd  29126  pthdepisspth  29828  pjoi0  31813  atomli  32478  archirng  33276  archiabllem1a  33279  archiabllem2a  33282  archiabl  33286  crefi  34038  pcmplfin  34051  sigaclcu  34308  measvun  34400  signsply0  34742  bnj1128  35179  bnj1204  35201  bnj1417  35230  neibastop2lem  36595  poimirlem31  38025  ftc1cnnclem  38065  sdclem2  38116  heibor1lem  38183  cvrat4  39942  hdmapval2  42331  ismrcd1  43154  relexpxpmin  44168  ee222  44953  ee333  44958  ee1111  44967  sbcoreleleq  44986  ordelordALT  44988  trsbc  44991  ee110  45128  ee101  45130  ee011  45132  ee100  45134  ee010  45136  ee001  45138  eel11111  45173  fnchoice  45484  fiiuncl  45520  mullimc  46068  islptre  46071  mullimcf  46075  addlimc  46098  stoweidlem20  46470  stoweidlem59  46509  perfectALTVlem2  48220