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  911  nfimd  1898  nfald  2322  cbv2w  2334  cbv2  2403  cbv2h  2406  exdistrf  2447  mo4  2561  euind  3721  reuind  3750  sbcimdv  3852  sbcimdvOLD  3853  cores  6249  tz7.7  6391  oprabidw  7440  tz7.49  8445  omsmolem  8656  phpOLD  9222  hta  9892  carddom2  9972  infdif  10204  isf32lem3  10350  alephval2  10567  cfpwsdom  10579  nqerf  10925  zeo  12648  o1rlimmul  15563  catideu  17619  catpropd  17653  ufileu  23423  iscau2  24794  scvxcvx  26490  issgon  33121  cvmsss2  34265  satffunlem2lem1  34395  onsucconni  35322  onsucsuccmpi  35328  bj-peircestab  35429  bj-cbvalimt  35516  bj-cbveximt  35517  bj-ax12v3ALT  35564  bj-wnf2  35596  bj-cbv2hv  35675  bj-sbsb  35715  bj-nfald  36018  lpolsatN  40359  lpolpolsatN  40360  naddcnffo  42114  frege70  42684  sspwtrALT  43583  snlindsntor  47152  0setrec  47749