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  9096  dffi3  9374  cantnflt  9624  cantnflem1  9641  axdc3lem2  10405  seqf1olem2  14052  wrd2ind  14733  relexpindlem  15073  rtrclind  15075  o1fsum  15824  lcmneg  16620  prmind2  16702  rami  17034  ramcl  17048  pslem  18587  telgsums  20016  islbs3  21205  psgndif  21634  mplsubglem  22030  mpllsslem  22031  gsummatr01lem4  22698  lmmo  23420  cnmpt12  23707  cnmpt22  23714  filss  23893  flimopn  24015  flimrest  24023  cfil3i  25311  equivcfil  25341  equivcau  25342  ovolicc2lem3  25561  limciun  25936  dvcnvrelem1  26059  dvfsumrlim  26073  dvfsum2  26076  dgrco  26315  scvxcvx  27027  ftalem3  27116  2sqlem6  27464  2sqlem8  27467  dchrisumlema  27529  dchrisumlem2  27531  addsproplem1  28039  negsproplem1  28098  gropd  29178  grstructd  29179  pthdepisspth  29881  pjoi0  31866  atomli  32531  archirng  33329  archiabllem1a  33332  archiabllem2a  33335  archiabl  33339  crefi  34105  pcmplfin  34118  sigaclcu  34375  measvun  34467  signsply0  34809  bnj1128  35249  bnj1204  35271  bnj1417  35300  neibastop2lem  36684  poimirlem31  38114  ftc1cnnclem  38154  sdclem2  38205  heibor1lem  38272  cvrat4  40031  hdmapval2  42420  ismrcd1  43243  relexpxpmin  44257  ee222  45042  ee333  45047  ee1111  45056  sbcoreleleq  45075  ordelordALT  45077  trsbc  45080  ee110  45217  ee101  45219  ee011  45221  ee100  45223  ee010  45225  ee001  45227  eel11111  45262  fnchoice  45573  fiiuncl  45609  mullimc  46156  islptre  46159  mullimcf  46163  addlimc  46186  stoweidlem20  46558  stoweidlem59  46597  perfectALTVlem2  48308