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  1609  ax11i  1692  equveli  1732  eupickbi  2079  rgen2a  2484  reu6  2868  sseq0  3399  disjel  3412  preq12b  3692  prel12  3693  prneimg  3696  elinti  3775  exmidundif  4124  opthreg  4466  elreldm  4760  issref  4916  relcnvtr  5053  relresfld  5063  funopg  5152  funimass2  5196  f0dom0  5311  fvimacnv  5528  elunirn  5660  oprabid  5796  op1steq  6070  f1o2ndf1  6118  reldmtpos  6143  rntpos  6147  nntri3or  6382  nnaordex  6416  nnawordex  6417  findcard2  6776  findcard2s  6777  mkvprop  7025  lt2addnq  7205  lt2mulnq  7206  genpelvl  7313  genpelvu  7314  distrlem5prl  7387  distrlem5pru  7388  caucvgprlemnkj  7467  map2psrprg  7606  rereceu  7690  ltxrlt  7823  0mnnnnn0  9002  elnnnn0b  9014  nn0le2is012  9126  btwnz  9163  uz11  9341  nn01to3  9402  zq  9411  xrltso  9575  xltnegi  9611  xnn0lenn0nn0  9641  xnn0xadd0  9643  iccleub  9707  fzdcel  9813  uznfz  9876  2ffzeq  9911  elfzonlteqm1  9980  flqeqceilz  10084  modqadd1  10127  modqmul1  10143  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  fzfig  10196  m1expeven  10333  caucvgrelemcau  10745  rexico  10986  fisumss  11154  fsum2dlemstep  11196  ntrivcvgap  11310  0dvds  11502  alzdvds  11541  opoe  11581  omoe  11582  opeo  11583  omeo  11584  m1exp1  11587  nn0enne  11588  nn0o1gt2  11591  gcdneg  11659  dfgcd2  11691  algcvgblem  11719  algcvga  11721  eucalglt  11727  coprmdvds  11762  divgcdcoprmex  11772  cncongr1  11773  prm2orodd  11796  tg2  12218  tgcl  12222  neii1  12305  neii2  12307  txlm  12437  reopnap  12696  tgioo  12704  addcncntoplem  12709  bj-elssuniab  12987  bj-nn0sucALT  13165  triap  13213