Theorem syl6bi 163

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 144	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.33bdc  1630  ax11i  1714  equveli  1759  eupickbi  2108  nfabdw  2338  rgen2a  2531  reu6  2927  sseq0  3465  disjel  3478  preq12b  3771  prel12  3772  prneimg  3775  elinti  3854  exmidundif  4207  opthreg  4556  elreldm  4854  issref  5012  relcnvtr  5149  relresfld  5159  funopg  5251  funimass2  5295  f0dom0  5410  fvimacnv  5632  elunirn  5767  oprabid  5907  op1steq  6180  f1o2ndf1  6229  reldmtpos  6254  rntpos  6258  nntri3or  6494  nnaordex  6529  nnawordex  6530  findcard2  6889  findcard2s  6890  mkvprop  7156  cc2lem  7265  lt2addnq  7403  lt2mulnq  7404  genpelvl  7511  genpelvu  7512  distrlem5prl  7585  distrlem5pru  7586  caucvgprlemnkj  7665  map2psrprg  7804  rereceu  7888  ltxrlt  8023  0mnnnnn0  9208  elnnnn0b  9220  nn0le2is012  9335  btwnz  9372  uz11  9550  nn01to3  9617  zq  9626  xrltso  9796  xltnegi  9835  xnn0lenn0nn0  9865  xnn0xadd0  9867  iccleub  9931  fzdcel  10040  uznfz  10103  2ffzeq  10141  elfzonlteqm1  10210  icogelb  10266  flqeqceilz  10318  modqadd1  10361  modqmul1  10377  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  fzfig  10430  m1expeven  10567  qsqeqor  10631  caucvgrelemcau  10989  rexico  11230  fisumss  11400  fsum2dlemstep  11442  ntrivcvgap  11556  fprodssdc  11598  fprod2dlemstep  11630  0dvds  11818  alzdvds  11860  opoe  11900  omoe  11901  opeo  11902  omeo  11903  m1exp1  11906  nn0enne  11907  nn0o1gt2  11910  gcdneg  11983  dfgcd2  12015  algcvgblem  12049  algcvga  12051  eucalglt  12057  coprmdvds  12092  divgcdcoprmex  12102  cncongr1  12103  prm2orodd  12126  prm23lt5  12263  pockthi  12356  f1ocpbl  12732  f1ovscpbl  12733  f1olecpbl  12734  ismnddef  12819  lmodfopnelem1  13414  tg2  13563  tgcl  13567  neii1  13650  neii2  13652  txlm  13782  reopnap  14041  tgioo  14049  addcncntoplem  14054  2lgsoddprmlem3  14462  bj-elssuniab  14546  bj-nn0sucALT  14733  triap  14780