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  1618  ax11i  1702  equveli  1747  eupickbi  2096  nfabdw  2326  rgen2a  2519  reu6  2914  sseq0  3449  disjel  3462  preq12b  3749  prel12  3750  prneimg  3753  elinti  3832  exmidundif  4184  opthreg  4532  elreldm  4829  issref  4985  relcnvtr  5122  relresfld  5132  funopg  5221  funimass2  5265  f0dom0  5380  fvimacnv  5599  elunirn  5733  oprabid  5870  op1steq  6144  f1o2ndf1  6192  reldmtpos  6217  rntpos  6221  nntri3or  6457  nnaordex  6491  nnawordex  6492  findcard2  6851  findcard2s  6852  mkvprop  7118  cc2lem  7203  lt2addnq  7341  lt2mulnq  7342  genpelvl  7449  genpelvu  7450  distrlem5prl  7523  distrlem5pru  7524  caucvgprlemnkj  7603  map2psrprg  7742  rereceu  7826  ltxrlt  7960  0mnnnnn0  9142  elnnnn0b  9154  nn0le2is012  9269  btwnz  9306  uz11  9484  nn01to3  9551  zq  9560  xrltso  9728  xltnegi  9767  xnn0lenn0nn0  9797  xnn0xadd0  9799  iccleub  9863  fzdcel  9971  uznfz  10034  2ffzeq  10072  elfzonlteqm1  10141  icogelb  10197  flqeqceilz  10249  modqadd1  10292  modqmul1  10308  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  fzfig  10361  m1expeven  10498  qsqeqor  10561  caucvgrelemcau  10918  rexico  11159  fisumss  11329  fsum2dlemstep  11371  ntrivcvgap  11485  fprodssdc  11527  fprod2dlemstep  11559  0dvds  11747  alzdvds  11788  opoe  11828  omoe  11829  opeo  11830  omeo  11831  m1exp1  11834  nn0enne  11835  nn0o1gt2  11838  gcdneg  11911  dfgcd2  11943  algcvgblem  11977  algcvga  11979  eucalglt  11985  coprmdvds  12020  divgcdcoprmex  12030  cncongr1  12031  prm2orodd  12054  prm23lt5  12191  pockthi  12284  tg2  12660  tgcl  12664  neii1  12747  neii2  12749  txlm  12879  reopnap  13138  tgioo  13146  addcncntoplem  13151  bj-elssuniab  13632  bj-nn0sucALT  13820  triap  13868