Theorem syl3c 64

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 63	. 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:  tfrlem1  7359  fodomr  7996  dffi3  8220  cantnflt  8452  cantnflem1c  8467  cantnflem1  8469  isfin2-2  9024  fin23lem17  9043  fin23lem39  9055  axdc3lem2  9156  ttukeylem5  9218  pwfseqlem5  9364  seqf1olem2  12703  wrdind  13328  wrd2ind  13329  relexpindlem  13651  rtrclind  13653  rlimclim1  14124  caucvgrlem  14251  o1fsum  14386  lcmneg  15154  prmind2  15236  rami  15557  ramcl  15571  poslubmo  16969  posglbmo  16970  pslem  17029  telgsums  18213  pgpfaclem2  18304  islbs3  18976  mplsubglem  19255  mpllsslem  19256  prmirredlem  19660  psgndif  19767  gsummatr01lem4  20283  lmcvg  20876  lmff  20915  lmmo  20994  1stcfb  21058  1stcelcls  21074  restnlly  21095  lly1stc  21109  kgeni  21150  cnmpt12  21280  cnmpt22  21287  filss  21467  flimopn  21589  flimrest  21597  tgpt0  21732  tsmsi  21747  tsmsxp  21768  nmoleub2lem2  22724  nmoleub3  22727  cfil3i  22875  equivcfil  22905  equivcau  22906  ovolicc2lem3  23094  ovolicc2  23097  vitalilem2  23184  vitalilem3  23185  itg2seq  23315  limciun  23464  dvferm1lem  23551  dvferm2lem  23553  dvcnvrelem1  23584  dvfsumrlim  23598  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  fta1glem2  23730  plyeq0lem  23770  dgrcolem2  23834  dgrco  23835  plydivlem4  23855  fta1lem  23866  vieta1  23871  scvxcvx  24512  wilthlem2  24595  ftalem3  24601  perfectlem2  24755  2sqlem6  24948  2sqlem8  24951  dchrisumlema  24977  dchrisumlem2  24979  gropd  25708  grstructd  25709  pthdepisspth  26104  pjoi0  27960  atomli  28625  archirng  29073  archiabllem1a  29076  archiabllem2a  29079  archiabl  29083  crefi  29242  pcmplfin  29255  sigaclcu  29507  measvun  29599  signsply0  29954  bnj1128  30312  bnj1204  30334  bnj1417  30363  neibastop2lem  31525  poimirlem31  32610  ftc1cnnclem  32653  sdclem2  32708  heibor1lem  32778  cvrat4  33747  hdmapval2  36142  ismrcd1  36279  relexpxpmin  37028  ee222  37729  ee333  37734  ee1111  37743  sbcoreleleq  37766  ordelordALT  37768  trsbc  37771  ee110  37923  ee101  37925  ee011  37927  ee100  37929  ee010  37931  ee001  37933  eel1111  37968  eel11111  37971  fnchoice  38211  fiiuncl  38259  mullimc  38683  islptre  38686  mullimcf  38690  addlimc  38715  stoweidlem20  38913  stoweidlem59  38952  perfectALTVlem2  40165  pthdepissPth  40941