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  912  nfimd  1894  nfald  2328  cbv2w  2339  cbv2  2408  cbv2h  2411  exdistrf  2452  mo4  2566  euind  3730  reuind  3759  sbcimdv  3859  cores  6269  tz7.7  6410  oprabidw  7462  tz7.49  8485  omsmolem  8695  phpOLD  9259  hta  9937  carddom2  10017  infdif  10248  isf32lem3  10395  alephval2  10612  cfpwsdom  10624  nqerf  10970  zeo  12704  o1rlimmul  15655  catideu  17718  catpropd  17752  ufileu  23927  iscau2  25311  scvxcvx  27029  issgon  34124  cbvex1v  35088  cvmsss2  35279  satffunlem2lem1  35409  onsucconni  36438  onsucsuccmpi  36444  bj-peircestab  36554  bj-cbvalimt  36640  bj-cbveximt  36641  bj-ax12v3ALT  36687  bj-wnf2  36719  bj-cbv2hv  36798  bj-sbsb  36838  bj-nfald  37138  lpolsatN  41490  lpolpolsatN  41491  naddcnffo  43377  frege70  43946  sspwtrALT  44842  snlindsntor  48388  0setrec  49223