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  912  nfimd  1896  nfald  2334  cbv2w  2342  cbv2  2408  cbv2h  2411  exdistrf  2452  mo4  2567  euind  3684  reuind  3713  sbcimdv  3811  cores  6215  tz7.7  6351  oprabidw  7399  tz7.49  8386  omsmolem  8595  hta  9821  carddom2  9901  infdif  10130  isf32lem3  10277  alephval2  10495  cfpwsdom  10507  nqerf  10853  zeo  12590  o1rlimmul  15554  catideu  17610  catpropd  17644  ufileu  23875  iscau2  25245  scvxcvx  26964  issgon  34300  cbvex1v  35249  cvmsss2  35487  satffunlem2lem1  35617  onsucconni  36650  onsucsuccmpi  36656  regsfromunir1  36689  bj-peircestab  36772  bj-cbvalimt  36872  bj-cbveximt  36873  bj-ax12v3ALT  36928  bj-wnf2  36960  bj-cbv2hv  37042  bj-sbsb  37082  bj-nfald  37387  lpolsatN  41861  lpolpolsatN  41862  naddcnffo  43718  frege70  44286  sspwtrALT  45174  snlindsntor  48828  0setrec  50060