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  2359  cbv2w  2367  cbv2  2433  cbv2h  2436  exdistrf  2477  mo4  2592  euind  3682  reuind  3711  sbcimdv  3807  cores  6249  tz7.7  6387  oprabidw  7449  tz7.49  8448  omsmolem  8659  hta  9955  htaOLD  9956  carddom2  10051  infdif  10279  isf32lem3  10426  alephval2  10650  cfpwsdom  10662  nqerf  11008  zeo  12778  o1rlimmul  15779  catideu  17842  catpropd  17876  ufileu  24231  iscau2  25591  scvxcvx  27306  issgon  34748  cbvex1v  35697  cvmsss2  36018  satffunlem2lem1  36148  onsucconni  37205  onsucsuccmpi  37211  dfttc4lem2  37297  regsfromunir1  37308  bj-peircestab  37400  bj-ax12v3ALT  37568  bj-wnf2  37602  bj-cbv2hv  37689  bj-sbsb  37729  bj-nfald  38036  lpolsatN  42525  lpolpolsatN  42526  naddcnffo  44350  frege70  44918  sspwtrALT  45789  snlindsntor  49552  0setrec  50766