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  1641  ax11i  1725  equveli  1770  eupickbi  2124  nfabdw  2355  rgen2a  2548  reu6  2949  sseq0  3488  disjel  3501  preq12b  3796  prel12  3797  prneimg  3800  elinti  3879  exmidundif  4235  opthreg  4588  elreldm  4888  issref  5048  relcnvtr  5185  relresfld  5195  funopg  5288  funimass2  5332  f0dom0  5447  fvimacnv  5673  elunirn  5809  oprabid  5950  op1steq  6232  f1o2ndf1  6281  reldmtpos  6306  rntpos  6310  nntri3or  6546  nnaordex  6581  nnawordex  6582  findcard2  6945  findcard2s  6946  mkvprop  7217  cc2lem  7326  lt2addnq  7464  lt2mulnq  7465  genpelvl  7572  genpelvu  7573  distrlem5prl  7646  distrlem5pru  7647  caucvgprlemnkj  7726  map2psrprg  7865  rereceu  7949  ltxrlt  8085  0mnnnnn0  9272  elnnnn0b  9284  nn0le2is012  9399  btwnz  9436  uz11  9615  nn01to3  9682  zq  9691  xrltso  9862  xltnegi  9901  xnn0lenn0nn0  9931  xnn0xadd0  9933  iccleub  9997  fzdcel  10106  uznfz  10169  2ffzeq  10207  elfzonlteqm1  10277  icogelb  10334  flqeqceilz  10389  modqadd1  10432  modqmul1  10448  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  fzfig  10501  seqf1og  10592  m1expeven  10657  qsqeqor  10721  caucvgrelemcau  11124  rexico  11365  fisumss  11535  fsum2dlemstep  11577  ntrivcvgap  11691  fprodssdc  11733  fprod2dlemstep  11765  0dvds  11954  alzdvds  11996  opoe  12036  omoe  12037  opeo  12038  omeo  12039  m1exp1  12042  nn0enne  12043  nn0o1gt2  12046  gcdneg  12119  dfgcd2  12151  algcvgblem  12187  algcvga  12189  eucalglt  12195  coprmdvds  12230  divgcdcoprmex  12240  cncongr1  12241  prm2orodd  12264  prm23lt5  12401  pockthi  12496  f1ocpbl  12894  f1ovscpbl  12895  f1olecpbl  12896  ismnddef  12999  lmodfopnelem1  13820  tg2  14228  tgcl  14232  neii1  14315  neii2  14317  txlm  14447  reopnap  14706  tgioo  14714  addcncntoplem  14719  gausslemma2dlem0i  15173  2lgsoddprmlem3  15199  bj-elssuniab  15283  bj-nn0sucALT  15470  triap  15519