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:  orim12dALT  936  nfimd  1993  sbi1v  2327  nfald  2351  nfeqf2OLD  2383  cbv2h  2408  exdistrf  2454  euind  3589  reuind  3609  sbcimdv  3695  cores  5857  tz7.7  5967  tz7.49  7779  omsmolem  7973  php  8386  hta  9010  carddom2  9089  infdif  9319  isf32lem3  9465  alephval2  9682  cfpwsdom  9694  nqerf  10040  zeo  11753  o1rlimmul  14690  catideu  16650  catpropd  16683  ufileu  22051  iscau2  23403  scvxcvx  25064  issgon  30702  cvmsss2  31773  onsucconni  32944  onsucsuccmpi  32950  bj-ssbft  33148  bj-ax12v3ALT  33182  bj-cbv2hv  33235  bj-sbsb  33319  lpolsatN  37509  lpolpolsatN  37510  frege70  39009  sspwtrALT  39818  snlindsntor  43059  0setrec  43249