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  912  nfimd  1896  nfald  2333  cbv2w  2341  cbv2  2407  cbv2h  2410  exdistrf  2451  mo4  2566  euind  3670  reuind  3699  sbcimdv  3797  cores  6213  tz7.7  6349  oprabidw  7398  tz7.49  8384  omsmolem  8593  hta  9821  carddom2  9901  infdif  10130  isf32lem3  10277  alephval2  10495  cfpwsdom  10507  nqerf  10853  zeo  12615  o1rlimmul  15581  catideu  17641  catpropd  17675  ufileu  23884  iscau2  25244  scvxcvx  26949  issgon  34267  cbvex1v  35216  cvmsss2  35456  satffunlem2lem1  35586  onsucconni  36619  onsucsuccmpi  36625  dfttc4lem2  36711  regsfromunir1  36722  bj-peircestab  36815  bj-ax12v3ALT  36983  bj-wnf2  37017  bj-cbv2hv  37104  bj-sbsb  37144  bj-nfald  37449  lpolsatN  41934  lpolpolsatN  41935  naddcnffo  43792  frege70  44360  sspwtrALT  45248  snlindsntor  48947  0setrec  50179