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  1891  nfald  2326  cbv2w  2337  cbv2  2405  cbv2h  2408  exdistrf  2449  mo4  2563  euind  3732  reuind  3761  sbcimdv  3864  sbcimdvOLD  3865  cores  6270  tz7.7  6411  oprabidw  7461  tz7.49  8483  omsmolem  8693  phpOLD  9256  hta  9934  carddom2  10014  infdif  10245  isf32lem3  10392  alephval2  10609  cfpwsdom  10621  nqerf  10967  zeo  12701  o1rlimmul  15651  catideu  17719  catpropd  17753  ufileu  23942  iscau2  25324  scvxcvx  27043  issgon  34103  cbvex1v  35066  cvmsss2  35258  satffunlem2lem1  35388  onsucconni  36419  onsucsuccmpi  36425  bj-peircestab  36535  bj-cbvalimt  36621  bj-cbveximt  36622  bj-ax12v3ALT  36668  bj-wnf2  36700  bj-cbv2hv  36779  bj-sbsb  36819  bj-nfald  37119  lpolsatN  41470  lpolpolsatN  41471  naddcnffo  43353  frege70  43922  sspwtrALT  44819  snlindsntor  48316  0setrec  48934