Theorem syl56 37

Description: Combine syl5 35 and syl6 36. (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 36	. 2 ⊢ (𝜒 → (𝜓 → 𝜏))
5	1, 4	syl5 35	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  924  nfimd  1924  nfald  2361  cbv2w  2369  cbv2  2435  cbv2h  2438  exdistrf  2479  mo4  2594  euind  3688  reuind  3717  sbcimdv  3813  cores  6252  tz7.7  6388  oprabidw  7443  tz7.49  8433  omsmolem  8644  hta  9884  carddom2  9964  infdif  10192  isf32lem3  10340  alephval2  10558  cfpwsdom  10570  nqerf  10916  zeo  12683  o1rlimmul  15672  catideu  17732  catpropd  17766  ufileu  24057  iscau2  25417  scvxcvx  27131  issgon  34494  cbvex1v  35443  cvmsss2  35747  satffunlem2lem1  35877  onsucconni  36929  onsucsuccmpi  36935  dfttc4lem2  37021  regsfromunir1  37032  bj-peircestab  37124  bj-ax12v3ALT  37292  bj-wnf2  37326  bj-cbv2hv  37413  bj-sbsb  37453  bj-nfald  37760  lpolsatN  42243  lpolpolsatN  42244  naddcnffo  44074  frege70  44642  sspwtrALT  45513  snlindsntor  49234  0setrec  50465