Theorem syl56 37

Description: Combine syl5 35 and syl6 36. (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 36	. 2 ⊢ (𝜒 → (𝜓 → 𝜏))
5	1, 4	syl5 35	1 ⊢ (𝜒 → (𝜑 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  orim12dALT  925  nfimd  1929  nfald  2362  cbv2w  2370  cbv2  2435  cbv2h  2438  exdistrf  2479  mo4  2594  euind  3685  reuind  3714  sbcimdv  3810  cores  6269  tz7.7  6414  oprabidw  7482  tz7.49  8493  omsmolem  8704  hta  9999  htaOLD  10000  carddom2  10095  infdif  10325  isf32lem3  10472  alephval2  10696  cfpwsdom  10708  nqerf  11054  zeo  12825  o1rlimmul  15830  catideu  17899  catpropd  17933  ufileu  24293  iscau2  25653  scvxcvx  27370  issgon  34866  cbvex1v  35815  cvmsss2  36247  satffunlem2lem1  36377  onsucconni  37440  onsucsuccmpi  37446  dfttc4lem2  37532  regsfromunir1  37543  bj-peircestab  37635  bj-ax12v3ALT  37803  bj-wnf2  37837  bj-cbv2hv  37924  bj-sbsb  37964  bj-nfald  38327  lpolsatN  42811  lpolpolsatN  42812  naddcnffo  44627  frege70  45194  sspwtrALT  46064  snlindsntor  49914  0setrec  51203