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  909  nfimd  1897  nfald  2322  cbv2w  2334  cbv2  2403  cbv2h  2406  exdistrf  2447  mo4  2566  vtoclgft  3492  euind  3659  reuind  3688  sbcimdv  3790  sbcimdvOLD  3791  cores  6153  tz7.7  6292  oprabidw  7306  tz7.49  8276  omsmolem  8487  phpOLD  9005  hta  9655  carddom2  9735  infdif  9965  isf32lem3  10111  alephval2  10328  cfpwsdom  10340  nqerf  10686  zeo  12406  o1rlimmul  15328  catideu  17384  catpropd  17418  ufileu  23070  iscau2  24441  scvxcvx  26135  issgon  32091  cvmsss2  33236  satffunlem2lem1  33366  onsucconni  34626  onsucsuccmpi  34632  bj-peircestab  34733  bj-cbvalimt  34820  bj-cbveximt  34821  bj-ax12v3ALT  34868  bj-wnf2  34900  bj-cbv2hv  34979  bj-sbsb  35020  bj-nfald  35308  lpolsatN  39502  lpolpolsatN  39503  frege70  41541  sspwtrALT  42442  snlindsntor  45812  0setrec  46409