Theorem syl6bi 161

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.33bdc  1566  ax11i  1649  equveli  1689  eupickbi  2030  rgen2a  2429  reu6  2804  sseq0  3324  disjel  3337  preq12b  3614  prel12  3615  prneimg  3618  elinti  3697  exmidundif  4035  opthreg  4372  elreldm  4661  issref  4814  relcnvtr  4950  relresfld  4960  funopg  5048  funimass2  5092  f0dom0  5204  fvimacnv  5414  elunirn  5545  oprabid  5681  op1steq  5949  f1o2ndf1  5993  reldmtpos  6018  rntpos  6022  nntri3or  6254  nnaordex  6286  nnawordex  6287  findcard2  6605  findcard2s  6606  lt2addnq  6963  lt2mulnq  6964  genpelvl  7071  genpelvu  7072  distrlem5prl  7145  distrlem5pru  7146  caucvgprlemnkj  7225  rereceu  7424  ltxrlt  7552  0mnnnnn0  8705  elnnnn0b  8717  btwnz  8865  uz11  9041  nn01to3  9102  zq  9111  xrltso  9266  xltnegi  9297  iccleub  9349  fzdcel  9454  uznfz  9517  2ffzeq  9552  elfzonlteqm1  9621  flqeqceilz  9725  modqadd1  9768  modqmul1  9784  frecuzrdgtcl  9819  frecuzrdgfunlem  9826  fzfig  9837  m1expeven  10002  caucvgrelemcau  10413  rexico  10654  fisumss  10784  fsum2dlemstep  10828  0dvds  11094  alzdvds  11133  opoe  11173  omoe  11174  opeo  11175  omeo  11176  m1exp1  11179  nn0enne  11180  nn0o1gt2  11183  gcdneg  11251  dfgcd2  11281  algcvgblem  11309  ialgcvga  11311  eucalglt  11317  coprmdvds  11352  divgcdcoprmex  11362  cncongr1  11363  prm2orodd  11386  bj-elssuniab  11691  bj-nn0sucALT  11873