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  33152  cvmsss2  34296  satffunlem2lem1  34426  onsucconni  35370  onsucsuccmpi  35376  bj-peircestab  35477  bj-cbvalimt  35564  bj-cbveximt  35565  bj-ax12v3ALT  35612  bj-wnf2  35644  bj-cbv2hv  35723  bj-sbsb  35763  bj-nfald  36066  lpolsatN  40407  lpolpolsatN  40408  naddcnffo  42162  frege70  42732  sspwtrALT  43631  snlindsntor  47200  0setrec  47797