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  9168  dffi3  9471  cantnflt  9712  cantnflem1  9729  axdc3lem2  10491  seqf1olem2  14083  wrd2ind  14761  relexpindlem  15102  rtrclind  15104  o1fsum  15849  lcmneg  16640  prmind2  16722  rami  17053  ramcl  17067  pslem  18617  telgsums  20011  islbs3  21157  psgndif  21620  mplsubglem  22019  mpllsslem  22020  gsummatr01lem4  22664  lmmo  23388  cnmpt12  23675  cnmpt22  23682  filss  23861  flimopn  23983  flimrest  23991  cfil3i  25303  equivcfil  25333  equivcau  25334  ovolicc2lem3  25554  limciun  25929  dvcnvrelem1  26056  dvfsumrlim  26072  dvfsum2  26075  dgrco  26315  scvxcvx  27029  ftalem3  27118  2sqlem6  27467  2sqlem8  27470  dchrisumlema  27532  dchrisumlem2  27534  addsproplem1  28002  negsproplem1  28060  gropd  29048  grstructd  29049  pthdepisspth  29755  pjoi0  31736  atomli  32401  archirng  33195  archiabllem1a  33198  archiabllem2a  33201  archiabl  33205  crefi  33846  pcmplfin  33859  sigaclcu  34118  measvun  34210  signsply0  34566  bnj1128  35004  bnj1204  35026  bnj1417  35055  neibastop2lem  36361  poimirlem31  37658  ftc1cnnclem  37698  sdclem2  37749  heibor1lem  37816  cvrat4  39445  hdmapval2  41834  ismrcd1  42709  relexpxpmin  43730  ee222  44522  ee333  44527  ee1111  44536  sbcoreleleq  44555  ordelordALT  44557  trsbc  44560  ee110  44697  ee101  44699  ee011  44701  ee100  44703  ee010  44705  ee001  44707  eel11111  44743  fnchoice  45034  fiiuncl  45070  mullimc  45631  islptre  45634  mullimcf  45638  addlimc  45663  stoweidlem20  46035  stoweidlem59  46074  perfectALTVlem2  47709