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  908  nfimd  1889  nfald  2313  cbv2w  2325  cbv2  2394  cbv2h  2397  exdistrf  2438  mo4  2552  euind  3712  reuind  3741  sbcimdv  3843  sbcimdvOLD  3844  cores  6238  tz7.7  6380  oprabidw  7432  tz7.49  8440  omsmolem  8651  phpOLD  9217  hta  9887  carddom2  9967  infdif  10199  isf32lem3  10345  alephval2  10562  cfpwsdom  10574  nqerf  10920  zeo  12644  o1rlimmul  15559  catideu  17617  catpropd  17651  ufileu  23744  iscau2  25126  scvxcvx  26833  issgon  33576  cvmsss2  34720  satffunlem2lem1  34850  onsucconni  35778  onsucsuccmpi  35784  bj-peircestab  35885  bj-cbvalimt  35972  bj-cbveximt  35973  bj-ax12v3ALT  36020  bj-wnf2  36052  bj-cbv2hv  36131  bj-sbsb  36171  bj-nfald  36474  lpolsatN  40815  lpolpolsatN  40816  naddcnffo  42569  frege70  43139  sspwtrALT  44038  snlindsntor  47306  0setrec  47903