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  1926  nfald  2358  cbv2w  2366  cbv2  2432  cbv2h  2435  exdistrf  2476  mo4  2591  euind  3681  reuind  3710  sbcimdv  3806  cores  6250  tz7.7  6388  oprabidw  7452  tz7.49  8459  omsmolem  8670  hta  9966  htaOLD  9967  carddom2  10062  infdif  10290  isf32lem3  10437  alephval2  10661  cfpwsdom  10673  nqerf  11019  zeo  12789  o1rlimmul  15792  catideu  17855  catpropd  17889  ufileu  24244  iscau2  25604  scvxcvx  27319  issgon  34802  cbvex1v  35751  cvmsss2  36126  satffunlem2lem1  36256  onsucconni  37318  onsucsuccmpi  37324  dfttc4lem2  37410  regsfromunir1  37421  bj-peircestab  37513  bj-ax12v3ALT  37681  bj-wnf2  37715  bj-cbv2hv  37802  bj-sbsb  37842  bj-nfald  38150  lpolsatN  42639  lpolpolsatN  42640  naddcnffo  44460  frege70  45027  sspwtrALT  45898  snlindsntor  49677  0setrec  50966