Theorem syl3c 67

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 66	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
6	1, 5	mpd 16	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  fodomr  9126  dffi3  9401  cantnflt  9651  cantnflem1  9668  axdc3lem2  10453  seqf1olem2  14098  wrd2ind  14784  relexpindlem  15126  rtrclind  15128  o1fsum  15891  lcmneg  16686  prmind2  16768  rami  17100  ramcl  17114  pslem  18653  telgsums  20094  islbs3  21316  psgndif  21789  mplsubglem  22185  mpllsslem  22186  gsummatr01lem4  22852  lmmo  23574  cnmpt12  23861  cnmpt22  23868  filss  24047  flimopn  24169  flimrest  24177  cfil3i  25465  equivcfil  25495  equivcau  25496  ovolicc2lem3  25715  limciun  26090  dvcnvrelem1  26213  dvfsumrlim  26227  dvfsum2  26230  dgrco  26469  scvxcvx  27187  ftalem3  27276  2sqlem6  27624  2sqlem8  27627  dchrisumlema  27689  dchrisumlem2  27691  addsproplem1  28199  negsproplem1  28258  gropd  29418  grstructd  29419  pthdepisspth  30121  pjoi0  32106  atomli  32771  archirng  33539  archiabllem1a  33542  archiabllem2a  33545  archiabl  33549  crefi  34268  pcmplfin  34281  sigaclcu  34538  measvun  34631  signsply0  34970  bnj1128  35410  bnj1204  35432  bnj1417  35461  neibastop2lem  36912  poimirlem31  38343  ftc1cnnclem  38383  sdclem2  38434  heibor1lem  38501  cvrat4  40258  hdmapval2  42647  ismrcd1  43470  relexpxpmin  44484  ee222  45252  ee333  45257  ee1111  45266  sbcoreleleq  45285  ordelordALT  45287  trsbc  45290  ee110  45427  ee101  45429  ee011  45431  ee100  45433  ee010  45435  ee001  45437  eel11111  45472  fnchoice  45790  fiiuncl  45826  mullimc  46373  islptre  46376  mullimcf  46380  addlimc  46403  stoweidlem20  46775  stoweidlem59  46814  perfectALTVlem2  48528