Theorem syl5ib 210

Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5ib.1	|- (ph -> ps)
syl5ib.2	|- (ch -> (ps <-> th))

Assertion

Ref	Expression
syl5ib	|- (ch -> (ph -> th))

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- (ph -> ps)
2		syl5ib.2	. . 3 |- (ch -> (ps <-> th))
3	2	biimpd 198	. 2 |- (ch -> (ps -> th))
4	1, 3	syl5 28	1 |- (ch -> (ph -> th))

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  syl5ibcom  211  syl5ibr  212  19.23tOLD  1819  nfsb4t  2080  ax11indalem  2197  ax11inda2ALT  2198  gencl  2888  spsbc  3059  eqsbc2  3104  ssnelpss  3614  adj11  3890  uniintsn  3964  phi011lem1  4599  optocl  4839  xpexr  5110  funimass1  5170  fneu  5188  dmfex  5248  fniniseg  5372  eqfnfv  5393  eqfnfv2  5394  elpreima  5408  fnasrn  5418  dffo4  5424  fconst5  5456  funiunfv  5468  dff13  5472  f1ocnvfv  5479  f1ocnvfvb  5480  ce0ncpw1  6186  cecl  6187  dflec3  6222  lenc  6224