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  1896  nfald  2334  cbv2w  2342  cbv2  2408  cbv2h  2411  exdistrf  2452  mo4  2567  euind  3671  reuind  3700  sbcimdv  3798  cores  6207  tz7.7  6343  oprabidw  7391  tz7.49  8377  omsmolem  8586  hta  9812  carddom2  9892  infdif  10121  isf32lem3  10268  alephval2  10486  cfpwsdom  10498  nqerf  10844  zeo  12606  o1rlimmul  15572  catideu  17632  catpropd  17666  ufileu  23894  iscau2  25254  scvxcvx  26963  issgon  34283  cbvex1v  35232  cvmsss2  35472  satffunlem2lem1  35602  onsucconni  36635  onsucsuccmpi  36641  dfttc4lem2  36727  regsfromunir1  36738  bj-peircestab  36831  bj-ax12v3ALT  36999  bj-wnf2  37033  bj-cbv2hv  37120  bj-sbsb  37160  bj-nfald  37465  lpolsatN  41948  lpolpolsatN  41949  naddcnffo  43810  frege70  44378  sspwtrALT  45266  snlindsntor  48959  0setrec  50191