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  9159  dffi3  9462  cantnflt  9703  cantnflem1  9720  axdc3lem2  10482  seqf1olem2  14047  wrd2ind  14713  relexpindlem  15050  rtrclind  15052  o1fsum  15799  lcmneg  16581  prmind2  16663  rami  16991  ramcl  17005  pslem  18571  telgsums  19955  islbs3  21050  psgndif  21541  mplsubglem  21948  mpllsslem  21949  gsummatr01lem4  22580  lmmo  23304  cnmpt12  23591  cnmpt22  23598  filss  23777  flimopn  23899  flimrest  23907  cfil3i  25217  equivcfil  25247  equivcau  25248  ovolicc2lem3  25468  limciun  25843  dvcnvrelem1  25970  dvfsumrlim  25986  dvfsum2  25989  dgrco  26230  scvxcvx  26938  ftalem3  27027  2sqlem6  27376  2sqlem8  27379  dchrisumlema  27441  dchrisumlem2  27443  addsproplem1  27906  negsproplem1  27960  gropd  28864  grstructd  28865  pthdepisspth  29569  pjoi0  31547  atomli  32212  archirng  32917  archiabllem1a  32920  archiabllem2a  32923  archiabl  32927  crefi  33481  pcmplfin  33494  sigaclcu  33769  measvun  33861  signsply0  34216  bnj1128  34654  bnj1204  34676  bnj1417  34705  neibastop2lem  35877  poimirlem31  37157  ftc1cnnclem  37197  sdclem2  37248  heibor1lem  37315  cvrat4  38948  hdmapval2  41337  ismrcd1  42149  relexpxpmin  43178  ee222  43972  ee333  43977  ee1111  43986  sbcoreleleq  44005  ordelordALT  44007  trsbc  44010  ee110  44147  ee101  44149  ee011  44151  ee100  44153  ee010  44155  ee001  44157  eel11111  44193  fnchoice  44422  fiiuncl  44460  mullimc  45033  islptre  45036  mullimcf  45040  addlimc  45065  stoweidlem20  45437  stoweidlem59  45476  perfectALTVlem2  47091