let x be Real; :: thesis: ( x <> 0 implies ( sinh x <> 0 & tanh x <> 0 ) )
A1: exp_R x > 0 by SIN_COS:55;
assume x <> 0 ; :: thesis: ( sinh x <> 0 & tanh x <> 0 )
then 1 / (exp_R x) <> exp_R x by A1, SIN_COS7:29, XCMPLX_1:199;
then ((exp_R x) - (exp_R (- x))) / 2 <> 0 by TAYLOR_1:4;
then A2: sinh x <> 0 by Lm2;
cosh x <> 0 by Lm1;
then (sinh x) / (cosh x) <> 0 by A2, XCMPLX_1:50;
hence ( sinh x <> 0 & tanh x <> 0 ) by Th1; :: thesis: verum