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  911  nfimd  1895  nfald  2331  cbv2w  2339  cbv2  2405  cbv2h  2408  exdistrf  2449  mo4  2563  euind  3679  reuind  3708  sbcimdv  3806  cores  6204  tz7.7  6340  oprabidw  7386  tz7.49  8373  omsmolem  8581  hta  9801  carddom2  9881  infdif  10110  isf32lem3  10257  alephval2  10474  cfpwsdom  10486  nqerf  10832  zeo  12569  o1rlimmul  15533  catideu  17589  catpropd  17623  ufileu  23854  iscau2  25224  scvxcvx  26943  issgon  34208  cbvex1v  35158  cvmsss2  35390  satffunlem2lem1  35520  onsucconni  36553  onsucsuccmpi  36559  bj-peircestab  36669  bj-cbvalimt  36755  bj-cbveximt  36756  bj-ax12v3ALT  36803  bj-wnf2  36835  bj-cbv2hv  36914  bj-sbsb  36954  bj-nfald  37254  lpolsatN  41660  lpolpolsatN  41661  naddcnffo  43521  frege70  44090  sspwtrALT  44978  snlindsntor  48633  0setrec  49865