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:  syl1111anc  873  fodomr  8386  dffi3  8612  cantnflt  8853  cantnflem1  8870  axdc3lem2  9595  seqf1olem2  13142  wrd2ind  13821  wrd2indOLD  13822  relexpindlem  14187  rtrclind  14189  o1fsum  14926  lcmneg  15696  prmind2  15777  rami  16097  ramcl  16111  pslem  17566  telgsums  18751  islbs3  19523  mplsubglem  19802  mpllsslem  19803  psgndif  20315  gsummatr01lem4  20840  lmmo  21562  cnmpt12  21848  cnmpt22  21855  filss  22034  flimopn  22156  flimrest  22164  cfil3i  23444  equivcfil  23474  equivcau  23475  ovolicc2lem3  23692  limciun  24064  dvcnvrelem1  24186  dvfsumrlim  24200  dvfsum2  24203  dgrco  24437  scvxcvx  25132  ftalem3  25221  2sqlem6  25568  2sqlem8  25571  dchrisumlema  25597  dchrisumlem2  25599  gropd  26336  grstructd  26337  pthdepisspth  27044  pjoi0  29127  atomli  29792  archirng  30283  archiabllem1a  30286  archiabllem2a  30289  archiabl  30293  crefi  30455  pcmplfin  30468  sigaclcu  30721  measvun  30813  signsply0  31171  bnj1128  31600  bnj1204  31622  bnj1417  31651  noprefixmo  32382  neibastop2lem  32888  poimirlem31  33979  ftc1cnnclem  34021  sdclem2  34075  heibor1lem  34145  cvrat4  35513  hdmapval2  37902  ismrcd1  38100  relexpxpmin  38845  ee222  39541  ee333  39546  ee1111  39555  sbcoreleleq  39574  ordelordALT  39576  trsbc  39579  ee110  39725  ee101  39727  ee011  39729  ee100  39731  ee010  39733  ee001  39735  eel11111  39772  fnchoice  40001  fiiuncl  40046  mullimc  40637  islptre  40640  mullimcf  40644  addlimc  40669  stoweidlem20  41025  stoweidlem59  41064  perfectALTVlem2  42475