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  8652  dffi3  8879  cantnflt  9119  cantnflem1  9136  axdc3lem2  9862  seqf1olem2  13406  wrd2ind  14076  relexpindlem  14414  rtrclind  14416  o1fsum  15160  lcmneg  15937  prmind2  16019  rami  16341  ramcl  16355  pslem  17808  telgsums  19106  islbs3  19920  psgndif  20291  mplsubglem  20672  mpllsslem  20673  gsummatr01lem4  21263  lmmo  21985  cnmpt12  22272  cnmpt22  22279  filss  22458  flimopn  22580  flimrest  22588  cfil3i  23873  equivcfil  23903  equivcau  23904  ovolicc2lem3  24123  limciun  24497  dvcnvrelem1  24620  dvfsumrlim  24634  dvfsum2  24637  dgrco  24872  scvxcvx  25571  ftalem3  25660  2sqlem6  26007  2sqlem8  26010  dchrisumlema  26072  dchrisumlem2  26074  gropd  26824  grstructd  26825  pthdepisspth  27524  pjoi0  29500  atomli  30165  archirng  30867  archiabllem1a  30870  archiabllem2a  30873  archiabl  30877  crefi  31200  pcmplfin  31213  sigaclcu  31486  measvun  31578  signsply0  31931  bnj1128  32372  bnj1204  32394  bnj1417  32423  noprefixmo  33315  neibastop2lem  33821  poimirlem31  35088  ftc1cnnclem  35128  sdclem2  35180  heibor1lem  35247  cvrat4  36739  hdmapval2  39128  ismrcd1  39639  relexpxpmin  40418  ee222  41208  ee333  41213  ee1111  41222  sbcoreleleq  41241  ordelordALT  41243  trsbc  41246  ee110  41383  ee101  41385  ee011  41387  ee100  41389  ee010  41391  ee001  41393  eel11111  41429  fnchoice  41658  fiiuncl  41699  mullimc  42258  islptre  42261  mullimcf  42265  addlimc  42290  stoweidlem20  42662  stoweidlem59  42701  perfectALTVlem2  44240