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  8670  dffi3  8897  cantnflt  9137  cantnflem1  9154  axdc3lem2  9875  seqf1olem2  13413  wrd2ind  14087  relexpindlem  14424  rtrclind  14426  o1fsum  15170  lcmneg  15949  prmind2  16031  rami  16353  ramcl  16367  pslem  17818  telgsums  19115  islbs3  19929  mplsubglem  20216  mpllsslem  20217  psgndif  20748  gsummatr01lem4  21269  lmmo  21990  cnmpt12  22277  cnmpt22  22284  filss  22463  flimopn  22585  flimrest  22593  cfil3i  23874  equivcfil  23904  equivcau  23905  ovolicc2lem3  24122  limciun  24494  dvcnvrelem1  24616  dvfsumrlim  24630  dvfsum2  24633  dgrco  24867  scvxcvx  25565  ftalem3  25654  2sqlem6  26001  2sqlem8  26004  dchrisumlema  26066  dchrisumlem2  26068  gropd  26818  grstructd  26819  pthdepisspth  27518  pjoi0  29496  atomli  30161  archirng  30819  archiabllem1a  30822  archiabllem2a  30825  archiabl  30829  crefi  31113  pcmplfin  31126  sigaclcu  31378  measvun  31470  signsply0  31823  bnj1128  32264  bnj1204  32286  bnj1417  32315  noprefixmo  33204  neibastop2lem  33710  poimirlem31  34925  ftc1cnnclem  34967  sdclem2  35019  heibor1lem  35089  cvrat4  36581  hdmapval2  38970  ismrcd1  39302  relexpxpmin  40069  ee222  40843  ee333  40848  ee1111  40857  sbcoreleleq  40876  ordelordALT  40878  trsbc  40881  ee110  41018  ee101  41020  ee011  41022  ee100  41024  ee010  41026  ee001  41028  eel11111  41064  fnchoice  41293  fiiuncl  41334  mullimc  41904  islptre  41907  mullimcf  41911  addlimc  41936  stoweidlem20  42312  stoweidlem59  42351  perfectALTVlem2  43894