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  1628  ax11i  1712  equveli  1757  eupickbi  2106  nfabdw  2336  rgen2a  2529  reu6  2924  sseq0  3462  disjel  3475  preq12b  3766  prel12  3767  prneimg  3770  elinti  3849  exmidundif  4201  opthreg  4549  elreldm  4846  issref  5003  relcnvtr  5140  relresfld  5150  funopg  5242  funimass2  5286  f0dom0  5401  fvimacnv  5623  elunirn  5757  oprabid  5897  op1steq  6170  f1o2ndf1  6219  reldmtpos  6244  rntpos  6248  nntri3or  6484  nnaordex  6519  nnawordex  6520  findcard2  6879  findcard2s  6880  mkvprop  7146  cc2lem  7240  lt2addnq  7378  lt2mulnq  7379  genpelvl  7486  genpelvu  7487  distrlem5prl  7560  distrlem5pru  7561  caucvgprlemnkj  7640  map2psrprg  7779  rereceu  7863  ltxrlt  7997  0mnnnnn0  9181  elnnnn0b  9193  nn0le2is012  9308  btwnz  9345  uz11  9523  nn01to3  9590  zq  9599  xrltso  9767  xltnegi  9806  xnn0lenn0nn0  9836  xnn0xadd0  9838  iccleub  9902  fzdcel  10010  uznfz  10073  2ffzeq  10111  elfzonlteqm1  10180  icogelb  10236  flqeqceilz  10288  modqadd1  10331  modqmul1  10347  frecuzrdgtcl  10382  frecuzrdgfunlem  10389  fzfig  10400  m1expeven  10537  qsqeqor  10600  caucvgrelemcau  10957  rexico  11198  fisumss  11368  fsum2dlemstep  11410  ntrivcvgap  11524  fprodssdc  11566  fprod2dlemstep  11598  0dvds  11786  alzdvds  11827  opoe  11867  omoe  11868  opeo  11869  omeo  11870  m1exp1  11873  nn0enne  11874  nn0o1gt2  11877  gcdneg  11950  dfgcd2  11982  algcvgblem  12016  algcvga  12018  eucalglt  12024  coprmdvds  12059  divgcdcoprmex  12069  cncongr1  12070  prm2orodd  12093  prm23lt5  12230  pockthi  12323  ismnddef  12685  tg2  13131  tgcl  13135  neii1  13218  neii2  13220  txlm  13350  reopnap  13609  tgioo  13617  addcncntoplem  13622  bj-elssuniab  14103  bj-nn0sucALT  14290  triap  14338