Theorem syl56 36

Description: Combine syl5 34 and syl6 35. (Contributed by NM, 14-Nov-2013.)

Hypotheses

Ref	Expression
syl56.1	⊢ (𝜑 → 𝜓)
syl56.2	⊢ (𝜒 → (𝜓 → 𝜃))
syl56.3	⊢ (𝜃 → 𝜏)

Assertion

Ref	Expression
syl56	⊢ (𝜒 → (𝜑 → 𝜏))

Proof of Theorem syl56

Step	Hyp	Ref	Expression
1		syl56.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl56.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3		syl56.3	. . 3 ⊢ (𝜃 → 𝜏)
4	2, 3	syl6 35	. 2 ⊢ (𝜒 → (𝜓 → 𝜏))
5	1, 4	syl5 34	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:  spfwOLD  2008  nfald  2201  cbv2h  2305  exdistrf  2364  euind  3426  reuind  3444  sbcimdv  3531  sbcimdvOLD  3532  cores  5676  tz7.7  5787  tz7.49  7585  omsmolem  7778  php  8185  hta  8798  carddom2  8841  infdif  9069  isf32lem3  9215  alephval2  9432  cfpwsdom  9444  nqerf  9790  zeo  11501  o1rlimmul  14393  catideu  16383  catpropd  16416  ufileu  21770  iscau2  23121  scvxcvx  24757  issgon  30314  cvmsss2  31382  onsucconni  32561  onsucsuccmpi  32567  bj-ssbft  32767  bj-ax12v3ALT  32801  bj-cbv2hv  32856  bj-sbsb  32949  wl-dveeq12  33441  lpolsatN  37094  lpolpolsatN  37095  frege70  38544  sspwtrALT  39366  snlindsntor  42585  0setrec  42775