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  8897  dffi3  9168  cantnflt  9408  cantnflem1  9425  axdc3lem2  10208  seqf1olem2  13761  wrd2ind  14434  relexpindlem  14772  rtrclind  14774  o1fsum  15523  lcmneg  16306  prmind2  16388  rami  16714  ramcl  16728  pslem  18288  telgsums  19592  islbs3  20415  psgndif  20805  mplsubglem  21203  mpllsslem  21204  gsummatr01lem4  21805  lmmo  22529  cnmpt12  22816  cnmpt22  22823  filss  23002  flimopn  23124  flimrest  23132  cfil3i  24431  equivcfil  24461  equivcau  24462  ovolicc2lem3  24681  limciun  25056  dvcnvrelem1  25179  dvfsumrlim  25193  dvfsum2  25196  dgrco  25434  scvxcvx  26133  ftalem3  26222  2sqlem6  26569  2sqlem8  26572  dchrisumlema  26634  dchrisumlem2  26636  gropd  27399  grstructd  27400  pthdepisspth  28099  pjoi0  30075  atomli  30740  archirng  31438  archiabllem1a  31441  archiabllem2a  31444  archiabl  31448  crefi  31793  pcmplfin  31806  sigaclcu  32081  measvun  32173  signsply0  32526  bnj1128  32966  bnj1204  32988  bnj1417  33017  neibastop2lem  34545  poimirlem31  35804  ftc1cnnclem  35844  sdclem2  35896  heibor1lem  35963  cvrat4  37453  hdmapval2  39842  ismrcd1  40517  relexpxpmin  41295  ee222  42092  ee333  42097  ee1111  42106  sbcoreleleq  42125  ordelordALT  42127  trsbc  42130  ee110  42267  ee101  42269  ee011  42271  ee100  42273  ee010  42275  ee001  42277  eel11111  42313  fnchoice  42542  fiiuncl  42583  mullimc  43128  islptre  43131  mullimcf  43135  addlimc  43160  stoweidlem20  43532  stoweidlem59  43571  perfectALTVlem2  45143