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  1895  nfald  2333  cbv2w  2341  cbv2  2407  cbv2h  2410  exdistrf  2451  mo4  2566  euind  3682  reuind  3711  sbcimdv  3809  cores  6207  tz7.7  6343  oprabidw  7389  tz7.49  8376  omsmolem  8585  hta  9809  carddom2  9889  infdif  10118  isf32lem3  10265  alephval2  10483  cfpwsdom  10495  nqerf  10841  zeo  12578  o1rlimmul  15542  catideu  17598  catpropd  17632  ufileu  23863  iscau2  25233  scvxcvx  26952  issgon  34280  cbvex1v  35230  cvmsss2  35468  satffunlem2lem1  35598  onsucconni  36631  onsucsuccmpi  36637  regsfromunir1  36670  bj-peircestab  36753  bj-cbvalimt  36839  bj-cbveximt  36840  bj-ax12v3ALT  36887  bj-wnf2  36919  bj-cbv2hv  36998  bj-sbsb  37038  bj-nfald  37342  lpolsatN  41748  lpolpolsatN  41749  naddcnffo  43606  frege70  44174  sspwtrALT  45062  snlindsntor  48717  0setrec  49949