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  2926  sseq0  3464  disjel  3477  preq12b  3769  prel12  3770  prneimg  3773  elinti  3852  exmidundif  4204  opthreg  4553  elreldm  4850  issref  5008  relcnvtr  5145  relresfld  5155  funopg  5247  funimass2  5291  f0dom0  5406  fvimacnv  5628  elunirn  5762  oprabid  5902  op1steq  6175  f1o2ndf1  6224  reldmtpos  6249  rntpos  6253  nntri3or  6489  nnaordex  6524  nnawordex  6525  findcard2  6884  findcard2s  6885  mkvprop  7151  cc2lem  7260  lt2addnq  7398  lt2mulnq  7399  genpelvl  7506  genpelvu  7507  distrlem5prl  7580  distrlem5pru  7581  caucvgprlemnkj  7660  map2psrprg  7799  rereceu  7883  ltxrlt  8017  0mnnnnn0  9202  elnnnn0b  9214  nn0le2is012  9329  btwnz  9366  uz11  9544  nn01to3  9611  zq  9620  xrltso  9790  xltnegi  9829  xnn0lenn0nn0  9859  xnn0xadd0  9861  iccleub  9925  fzdcel  10033  uznfz  10096  2ffzeq  10134  elfzonlteqm1  10203  icogelb  10259  flqeqceilz  10311  modqadd1  10354  modqmul1  10370  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  fzfig  10423  m1expeven  10560  qsqeqor  10623  caucvgrelemcau  10980  rexico  11221  fisumss  11391  fsum2dlemstep  11433  ntrivcvgap  11547  fprodssdc  11589  fprod2dlemstep  11621  0dvds  11809  alzdvds  11850  opoe  11890  omoe  11891  opeo  11892  omeo  11893  m1exp1  11896  nn0enne  11897  nn0o1gt2  11900  gcdneg  11973  dfgcd2  12005  algcvgblem  12039  algcvga  12041  eucalglt  12047  coprmdvds  12082  divgcdcoprmex  12092  cncongr1  12093  prm2orodd  12116  prm23lt5  12253  pockthi  12346  ismnddef  12749  tg2  13342  tgcl  13346  neii1  13429  neii2  13431  txlm  13561  reopnap  13820  tgioo  13828  addcncntoplem  13833  bj-elssuniab  14314  bj-nn0sucALT  14501  triap  14548