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  1927  nfald  2358  cbv2w  2366  cbv2  2432  cbv2h  2435  exdistrf  2476  mo4  2591  euind  3682  reuind  3711  sbcimdv  3807  cores  6245  tz7.7  6383  oprabidw  7444  tz7.49  8434  omsmolem  8645  hta  9901  htaOLD  9902  carddom2  9982  infdif  10210  isf32lem3  10357  alephval2  10581  cfpwsdom  10593  nqerf  10939  zeo  12707  o1rlimmul  15706  catideu  17763  catpropd  17797  ufileu  24145  iscau2  25505  scvxcvx  27222  issgon  34633  cbvex1v  35583  cvmsss2  35853  satffunlem2lem1  35983  onsucconni  37056  onsucsuccmpi  37062  dfttc4lem2  37148  regsfromunir1  37159  bj-peircestab  37251  bj-ax12v3ALT  37419  bj-wnf2  37453  bj-cbv2hv  37540  bj-sbsb  37580  bj-nfald  37887  lpolsatN  42361  lpolpolsatN  42362  naddcnffo  44205  frege70  44773  sspwtrALT  45644  snlindsntor  49401  0setrec  50630