Theorem syl6bi 162

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

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

Assertion

Ref	Expression
syl6bi	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 143	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.33bdc  1610  ax11i  1693  equveli  1733  eupickbi  2082  rgen2a  2489  reu6  2877  sseq0  3409  disjel  3422  preq12b  3705  prel12  3706  prneimg  3709  elinti  3788  exmidundif  4137  opthreg  4479  elreldm  4773  issref  4929  relcnvtr  5066  relresfld  5076  funopg  5165  funimass2  5209  f0dom0  5324  fvimacnv  5543  elunirn  5675  oprabid  5811  op1steq  6085  f1o2ndf1  6133  reldmtpos  6158  rntpos  6162  nntri3or  6397  nnaordex  6431  nnawordex  6432  findcard2  6791  findcard2s  6792  mkvprop  7040  cc2lem  7098  lt2addnq  7236  lt2mulnq  7237  genpelvl  7344  genpelvu  7345  distrlem5prl  7418  distrlem5pru  7419  caucvgprlemnkj  7498  map2psrprg  7637  rereceu  7721  ltxrlt  7854  0mnnnnn0  9033  elnnnn0b  9045  nn0le2is012  9157  btwnz  9194  uz11  9372  nn01to3  9436  zq  9445  xrltso  9612  xltnegi  9648  xnn0lenn0nn0  9678  xnn0xadd0  9680  iccleub  9744  fzdcel  9851  uznfz  9914  2ffzeq  9949  elfzonlteqm1  10018  flqeqceilz  10122  modqadd1  10165  modqmul1  10181  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  fzfig  10234  m1expeven  10371  caucvgrelemcau  10784  rexico  11025  fisumss  11193  fsum2dlemstep  11235  ntrivcvgap  11349  0dvds  11549  alzdvds  11588  opoe  11628  omoe  11629  opeo  11630  omeo  11631  m1exp1  11634  nn0enne  11635  nn0o1gt2  11638  gcdneg  11706  dfgcd2  11738  algcvgblem  11766  algcvga  11768  eucalglt  11774  coprmdvds  11809  divgcdcoprmex  11819  cncongr1  11820  prm2orodd  11843  tg2  12268  tgcl  12272  neii1  12355  neii2  12357  txlm  12487  reopnap  12746  tgioo  12754  addcncntoplem  12759  bj-elssuniab  13169  bj-nn0sucALT  13347  triap  13399