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 ⊢ (𝜑 → 𝜏)

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  9104  dffi3  9379  cantnflt  9629  cantnflem1  9646  axdc3lem2  10423  seqf1olem2  14069  wrd2ind  14750  relexpindlem  15090  rtrclind  15092  o1fsum  15855  lcmneg  16651  prmind2  16733  rami  17065  ramcl  17079  pslem  18618  telgsums  20054  islbs3  21248  psgndif  21712  mplsubglem  22108  mpllsslem  22109  gsummatr01lem4  22776  lmmo  23498  cnmpt12  23785  cnmpt22  23792  filss  23971  flimopn  24093  flimrest  24101  cfil3i  25389  equivcfil  25419  equivcau  25420  ovolicc2lem3  25639  limciun  26014  dvcnvrelem1  26137  dvfsumrlim  26151  dvfsum2  26154  dgrco  26393  scvxcvx  27108  ftalem3  27197  2sqlem6  27545  2sqlem8  27548  dchrisumlema  27610  dchrisumlem2  27612  addsproplem1  28120  negsproplem1  28179  gropd  29290  grstructd  29291  pthdepisspth  29993  pjoi0  31978  atomli  32643  archirng  33421  archiabllem1a  33424  archiabllem2a  33427  archiabl  33431  crefi  34154  pcmplfin  34167  sigaclcu  34424  measvun  34516  signsply0  34855  bnj1128  35295  bnj1204  35317  bnj1417  35346  neibastop2lem  36733  poimirlem31  38162  ftc1cnnclem  38202  sdclem2  38253  heibor1lem  38320  cvrat4  40079  hdmapval2  42468  ismrcd1  43291  relexpxpmin  44305  ee222  45076  ee333  45081  ee1111  45090  sbcoreleleq  45109  ordelordALT  45111  trsbc  45114  ee110  45251  ee101  45253  ee011  45255  ee100  45257  ee010  45259  ee001  45261  eel11111  45296  fnchoice  45607  fiiuncl  45643  mullimc  46190  islptre  46193  mullimcf  46197  addlimc  46220  stoweidlem20  46592  stoweidlem59  46631  perfectALTVlem2  48342