Theorem biimtrdi 163

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
biimtrdi.1	|- ( ph -> ( ps <-> ch ) )
biimtrdi.2	|- ( ch -> th )

Assertion

Ref	Expression
biimtrdi	|- ( ph -> ( ps -> th ) )

Proof of Theorem biimtrdi

Step	Hyp	Ref	Expression
1		biimtrdi.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 144	. 2 |- ( ph -> ( ps -> ch ) )
3		biimtrdi.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  1644  ax11i  1728  equveli  1773  eupickbi  2127  nfabdw  2358  rgen2a  2551  reu6  2953  sseq0  3493  disjel  3506  preq12b  3801  prel12  3802  prneimg  3805  elinti  3884  exmidundif  4240  opthreg  4593  elreldm  4893  issref  5053  relcnvtr  5190  relresfld  5200  funopg  5293  funimass2  5337  f0dom0  5454  fvimacnv  5680  elunirn  5816  oprabid  5957  op1steq  6246  f1o2ndf1  6295  reldmtpos  6320  rntpos  6324  nntri3or  6560  nnaordex  6595  nnawordex  6596  findcard2  6959  findcard2s  6960  mkvprop  7233  cc2lem  7349  lt2addnq  7488  lt2mulnq  7489  genpelvl  7596  genpelvu  7597  distrlem5prl  7670  distrlem5pru  7671  caucvgprlemnkj  7750  map2psrprg  7889  rereceu  7973  ltxrlt  8109  0mnnnnn0  9298  elnnnn0b  9310  nn0le2is012  9425  btwnz  9462  uz11  9641  nn01to3  9708  zq  9717  xrltso  9888  xltnegi  9927  xnn0lenn0nn0  9957  xnn0xadd0  9959  iccleub  10023  fzdcel  10132  uznfz  10195  2ffzeq  10233  elfzonlteqm1  10303  icogelb  10372  flqeqceilz  10427  modqadd1  10470  modqmul1  10486  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  fzfig  10539  seqf1og  10630  m1expeven  10695  qsqeqor  10759  caucvgrelemcau  11162  rexico  11403  fisumss  11574  fsum2dlemstep  11616  ntrivcvgap  11730  fprodssdc  11772  fprod2dlemstep  11804  0dvds  11993  alzdvds  12036  opoe  12077  omoe  12078  opeo  12079  omeo  12080  m1exp1  12083  nn0enne  12084  nn0o1gt2  12087  gcdneg  12174  dfgcd2  12206  algcvgblem  12242  algcvga  12244  eucalglt  12250  coprmdvds  12285  divgcdcoprmex  12295  cncongr1  12296  prm2orodd  12319  prm23lt5  12457  pockthi  12552  f1ocpbl  13013  f1ovscpbl  13014  f1olecpbl  13015  ismnddef  13120  lmodfopnelem1  13956  tg2  14380  tgcl  14384  neii1  14467  neii2  14469  txlm  14599  reopnap  14866  tgioo  14874  addcncntoplem  14881  gausslemma2dlem0i  15382  2lgslem2  15417  2lgs  15429  2lgsoddprmlem3  15436  bj-elssuniab  15521  bj-nn0sucALT  15708  triap  15760