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  1679  ax11i  1762  equveli  1808  eupickbi  2165  nfabdw  2405  rgen2a  2598  reu6  3009  sseq0  3554  disjel  3567  preq12b  3879  prel12  3880  prneimg  3883  elinti  3963  exmidundif  4324  opthreg  4683  elreldm  4988  issref  5150  relcnvtr  5287  relresfld  5297  funopg  5391  funimass2  5439  f0dom0  5566  fvimacnv  5798  funopdmsn  5869  elunirn  5945  oprabid  6090  op1steq  6386  f1o2ndf1  6437  fvn0elsuppb  6465  suppfnss  6470  reldmtpos  6497  rntpos  6501  nntri3or  6739  nnaordex  6774  nnawordex  6775  findcard2  7159  findcard2s  7160  mkvprop  7462  cc2lem  7596  lt2addnq  7735  lt2mulnq  7736  genpelvl  7843  genpelvu  7844  distrlem5prl  7917  distrlem5pru  7918  caucvgprlemnkj  7997  map2psrprg  8136  rereceu  8220  ltxrlt  8355  0mnnnnn0  9545  elnnnn0b  9557  nn0le2is012  9678  btwnz  9715  uz11  9895  nn01to3  9967  zq  9976  xrltso  10148  xltnegi  10187  xnn0lenn0nn0  10217  xnn0xadd0  10219  iccleub  10283  fzdcel  10394  uznfz  10459  2ffzeq  10497  elfzonlteqm1  10577  icogelb  10649  flqeqceilz  10704  modqadd1  10747  modqmul1  10763  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  fzfig  10816  seqf1og  10907  m1expeven  10972  qsqeqor  11036  fundm2domnop0  11245  ccatrcl1  11327  pfxsuff1eqwrdeq  11416  wrdind  11439  wrd2ind  11440  swrdccat3blem  11456  caucvgrelemcau  11690  rexico  11931  fisumss  12103  fsum2dlemstep  12145  ntrivcvgap  12259  fprodssdc  12301  fprod2dlemstep  12333  0dvds  12522  alzdvds  12565  opoe  12606  omoe  12607  opeo  12608  omeo  12609  m1exp1  12612  nn0enne  12613  nn0o1gt2  12616  gcdneg  12703  dfgcd2  12735  algcvgblem  12771  algcvga  12773  eucalglt  12779  coprmdvds  12814  divgcdcoprmex  12824  cncongr1  12825  prm2orodd  12848  prm23lt5  12986  pockthi  13081  ballotfilemfc0  13176  ballotfilemfcc  13177  f1ocpbl  13575  f1ovscpbl  13576  f1olecpbl  13577  ismnddef  13679  lmodfopnelem1  14598  tg2  15051  tgcl  15055  neii1  15138  neii2  15140  txlm  15270  reopnap  15537  tgioo  15545  addcncntoplem  15552  gausslemma2dlem0i  16056  2lgslem2  16091  2lgs  16103  2lgsoddprmlem3  16110  uhgr0vb  16205  umgredg  16266  uspgrushgr  16301  uspgrupgr  16302  usgruspgr  16304  uhgr2edg  16327  edg0usgr  16368  egrsubgr  16384  0uhgrsubgr  16386  uhgrspansubgrlem  16397  vtxdg0v  16415  wlkpropg  16445  wlkv  16447  wlkvg  16449  wlkvtxeledgg  16465  wlkl1loop  16479  upgrwlkedg  16482  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  wlkv0  16490  clwwlkccat  16522  clwwlknp  16538  clwwlkext2edg  16543  eupth2lem3lem4fi  16594  bj-elssuniab  16689  bj-nn0sucALT  16874  triap  16939