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  897  nfimd  1973  spfwOLD  2122  nfald  2327  cbv2h  2430  nfeqf2  2452  exdistrf  2483  euind  3545  reuind  3563  sbcimdv  3649  cores  5781  tz7.7  5891  tz7.49  7697  omsmolem  7891  php  8304  hta  8928  carddom2  9007  infdif  9237  isf32lem3  9383  alephval2  9600  cfpwsdom  9612  nqerf  9958  zeo  11670  o1rlimmul  14557  catideu  16543  catpropd  16576  ufileu  21943  iscau2  23294  scvxcvx  24933  issgon  30526  cvmsss2  31594  onsucconni  32773  onsucsuccmpi  32779  bj-ssbft  32978  bj-ax12v3ALT  33012  bj-cbv2hv  33066  bj-sbsb  33158  lpolsatN  37296  lpolpolsatN  37297  frege70  38751  sspwtrALT  39572  snlindsntor  42783  0setrec  42973