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  1653  ax11i  1737  equveli  1782  eupickbi  2136  nfabdw  2367  rgen2a  2560  reu6  2962  sseq0  3502  disjel  3515  preq12b  3811  prel12  3812  prneimg  3815  elinti  3894  exmidundif  4251  opthreg  4605  elreldm  4905  issref  5066  relcnvtr  5203  relresfld  5213  funopg  5306  funimass2  5353  f0dom0  5471  fvimacnv  5697  funopdmsn  5766  elunirn  5837  oprabid  5978  op1steq  6267  f1o2ndf1  6316  reldmtpos  6341  rntpos  6345  nntri3or  6581  nnaordex  6616  nnawordex  6617  findcard2  6988  findcard2s  6989  mkvprop  7262  cc2lem  7380  lt2addnq  7519  lt2mulnq  7520  genpelvl  7627  genpelvu  7628  distrlem5prl  7701  distrlem5pru  7702  caucvgprlemnkj  7781  map2psrprg  7920  rereceu  8004  ltxrlt  8140  0mnnnnn0  9329  elnnnn0b  9341  nn0le2is012  9457  btwnz  9494  uz11  9673  nn01to3  9740  zq  9749  xrltso  9920  xltnegi  9959  xnn0lenn0nn0  9989  xnn0xadd0  9991  iccleub  10055  fzdcel  10164  uznfz  10227  2ffzeq  10265  elfzonlteqm1  10341  icogelb  10410  flqeqceilz  10465  modqadd1  10508  modqmul1  10524  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  fzfig  10577  seqf1og  10668  m1expeven  10733  qsqeqor  10797  fundm2domnop0  10992  pfxsuff1eqwrdeq  11153  caucvgrelemcau  11324  rexico  11565  fisumss  11736  fsum2dlemstep  11778  ntrivcvgap  11892  fprodssdc  11934  fprod2dlemstep  11966  0dvds  12155  alzdvds  12198  opoe  12239  omoe  12240  opeo  12241  omeo  12242  m1exp1  12245  nn0enne  12246  nn0o1gt2  12249  gcdneg  12336  dfgcd2  12368  algcvgblem  12404  algcvga  12406  eucalglt  12412  coprmdvds  12447  divgcdcoprmex  12457  cncongr1  12458  prm2orodd  12481  prm23lt5  12619  pockthi  12714  f1ocpbl  13176  f1ovscpbl  13177  f1olecpbl  13178  ismnddef  13283  lmodfopnelem1  14119  tg2  14565  tgcl  14569  neii1  14652  neii2  14654  txlm  14784  reopnap  15051  tgioo  15059  addcncntoplem  15066  gausslemma2dlem0i  15567  2lgslem2  15602  2lgs  15614  2lgsoddprmlem3  15621  bj-elssuniab  15764  bj-nn0sucALT  15951  triap  16005