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  1894  nfald  2328  cbv2w  2338  cbv2  2407  cbv2h  2410  exdistrf  2451  mo4  2565  euind  3707  reuind  3736  sbcimdv  3834  cores  6238  tz7.7  6378  oprabidw  7436  tz7.49  8459  omsmolem  8669  phpOLD  9231  hta  9911  carddom2  9991  infdif  10222  isf32lem3  10369  alephval2  10586  cfpwsdom  10598  nqerf  10944  zeo  12679  o1rlimmul  15635  catideu  17687  catpropd  17721  ufileu  23857  iscau2  25229  scvxcvx  26948  issgon  34154  cbvex1v  35105  cvmsss2  35296  satffunlem2lem1  35426  onsucconni  36455  onsucsuccmpi  36461  bj-peircestab  36571  bj-cbvalimt  36657  bj-cbveximt  36658  bj-ax12v3ALT  36704  bj-wnf2  36736  bj-cbv2hv  36815  bj-sbsb  36855  bj-nfald  37155  lpolsatN  41507  lpolpolsatN  41508  naddcnffo  43388  frege70  43957  sspwtrALT  44846  snlindsntor  48447  0setrec  49568