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  1678  ax11i  1762  equveli  1807  eupickbi  2162  nfabdw  2393  rgen2a  2586  reu6  2995  sseq0  3536  disjel  3549  preq12b  3853  prel12  3854  prneimg  3857  elinti  3937  exmidundif  4296  opthreg  4654  elreldm  4958  issref  5119  relcnvtr  5256  relresfld  5266  funopg  5360  funimass2  5408  f0dom0  5530  fvimacnv  5762  funopdmsn  5834  elunirn  5907  oprabid  6050  op1steq  6342  f1o2ndf1  6393  reldmtpos  6419  rntpos  6423  nntri3or  6661  nnaordex  6696  nnawordex  6697  findcard2  7078  findcard2s  7079  mkvprop  7357  cc2lem  7485  lt2addnq  7624  lt2mulnq  7625  genpelvl  7732  genpelvu  7733  distrlem5prl  7806  distrlem5pru  7807  caucvgprlemnkj  7886  map2psrprg  8025  rereceu  8109  ltxrlt  8245  0mnnnnn0  9434  elnnnn0b  9446  nn0le2is012  9562  btwnz  9599  uz11  9779  nn01to3  9851  zq  9860  xrltso  10031  xltnegi  10070  xnn0lenn0nn0  10100  xnn0xadd0  10102  iccleub  10166  fzdcel  10275  uznfz  10338  2ffzeq  10376  elfzonlteqm1  10456  icogelb  10526  flqeqceilz  10581  modqadd1  10624  modqmul1  10640  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  fzfig  10693  seqf1og  10784  m1expeven  10849  qsqeqor  10913  fundm2domnop0  11113  ccatrcl1  11195  pfxsuff1eqwrdeq  11284  wrdind  11307  wrd2ind  11308  swrdccat3blem  11324  caucvgrelemcau  11558  rexico  11799  fisumss  11971  fsum2dlemstep  12013  ntrivcvgap  12127  fprodssdc  12169  fprod2dlemstep  12201  0dvds  12390  alzdvds  12433  opoe  12474  omoe  12475  opeo  12476  omeo  12477  m1exp1  12480  nn0enne  12481  nn0o1gt2  12484  gcdneg  12571  dfgcd2  12603  algcvgblem  12639  algcvga  12641  eucalglt  12647  coprmdvds  12682  divgcdcoprmex  12692  cncongr1  12693  prm2orodd  12716  prm23lt5  12854  pockthi  12949  f1ocpbl  13412  f1ovscpbl  13413  f1olecpbl  13414  ismnddef  13519  lmodfopnelem1  14357  tg2  14803  tgcl  14807  neii1  14890  neii2  14892  txlm  15022  reopnap  15289  tgioo  15297  addcncntoplem  15304  gausslemma2dlem0i  15805  2lgslem2  15840  2lgs  15852  2lgsoddprmlem3  15859  uhgr0vb  15954  umgredg  16015  uspgrushgr  16050  uspgrupgr  16051  usgruspgr  16053  uhgr2edg  16076  edg0usgr  16117  egrsubgr  16133  0uhgrsubgr  16135  uhgrspansubgrlem  16146  vtxdg0v  16164  wlkpropg  16194  wlkv  16196  wlkvg  16198  wlkvtxeledgg  16214  wlkl1loop  16228  upgrwlkedg  16231  upgrwlkvtxedg  16234  uspgr2wlkeq  16235  wlkv0  16239  clwwlkccat  16271  clwwlknp  16287  clwwlkext2edg  16292  eupth2lem3lem4fi  16343  bj-elssuniab  16438  bj-nn0sucALT  16624  triap  16684