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  1898  nfald  2326  cbv2w  2336  cbv2  2403  cbv2h  2406  exdistrf  2447  mo4  2566  vtoclgft  3482  euind  3654  reuind  3683  sbcimdv  3786  sbcimdvOLD  3787  cores  6142  tz7.7  6277  oprabidw  7286  tz7.49  8246  omsmolem  8447  php  8897  hta  9586  carddom2  9666  infdif  9896  isf32lem3  10042  alephval2  10259  cfpwsdom  10271  nqerf  10617  zeo  12336  o1rlimmul  15256  catideu  17301  catpropd  17335  ufileu  22978  iscau2  24346  scvxcvx  26040  issgon  31991  cvmsss2  33136  satffunlem2lem1  33266  onsucconni  34553  onsucsuccmpi  34559  bj-peircestab  34660  bj-cbvalimt  34747  bj-cbveximt  34748  bj-ax12v3ALT  34795  bj-wnf2  34827  bj-cbv2hv  34906  bj-sbsb  34947  bj-nfald  35235  lpolsatN  39429  lpolpolsatN  39430  frege70  41430  sspwtrALT  42331  snlindsntor  45700  0setrec  46295