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  1895  sbi1vOLD  2317  nfald  2336  cbv2w  2346  cbv2  2412  cbv2h  2415  exdistrf  2458  mo4  2625  vtoclgft  3501  euind  3663  reuind  3692  sbcimdv  3789  cores  6069  tz7.7  6185  oprabidw  7166  tz7.49  8064  omsmolem  8263  php  8685  hta  9310  carddom2  9390  infdif  9620  isf32lem3  9766  alephval2  9983  cfpwsdom  9995  nqerf  10341  zeo  12056  o1rlimmul  14967  catideu  16938  catpropd  16971  ufileu  22524  iscau2  23881  scvxcvx  25571  issgon  31492  cvmsss2  32634  satffunlem2lem1  32764  onsucconni  33898  onsucsuccmpi  33904  bj-peircestab  34001  bj-cbvalimt  34085  bj-cbveximt  34086  bj-ax12v3ALT  34133  bj-wnf2  34165  bj-cbv2hv  34234  bj-sbsb  34275  bj-nfald  34552  lpolsatN  38784  lpolpolsatN  38785  frege70  40634  sspwtrALT  41528  snlindsntor  44880  0setrec  45233