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  1676  ax11i  1760  equveli  1805  eupickbi  2160  nfabdw  2391  rgen2a  2584  reu6  2993  sseq0  3534  disjel  3547  preq12b  3849  prel12  3850  prneimg  3853  elinti  3933  exmidundif  4292  opthreg  4650  elreldm  4954  issref  5115  relcnvtr  5252  relresfld  5262  funopg  5356  funimass2  5403  f0dom0  5525  fvimacnv  5756  funopdmsn  5827  elunirn  5900  oprabid  6043  op1steq  6335  f1o2ndf1  6386  reldmtpos  6412  rntpos  6416  nntri3or  6654  nnaordex  6689  nnawordex  6690  findcard2  7069  findcard2s  7070  mkvprop  7346  cc2lem  7473  lt2addnq  7612  lt2mulnq  7613  genpelvl  7720  genpelvu  7721  distrlem5prl  7794  distrlem5pru  7795  caucvgprlemnkj  7874  map2psrprg  8013  rereceu  8097  ltxrlt  8233  0mnnnnn0  9422  elnnnn0b  9434  nn0le2is012  9550  btwnz  9587  uz11  9767  nn01to3  9839  zq  9848  xrltso  10019  xltnegi  10058  xnn0lenn0nn0  10088  xnn0xadd0  10090  iccleub  10154  fzdcel  10263  uznfz  10326  2ffzeq  10364  elfzonlteqm1  10443  icogelb  10513  flqeqceilz  10568  modqadd1  10611  modqmul1  10627  frecuzrdgtcl  10662  frecuzrdgfunlem  10669  fzfig  10680  seqf1og  10771  m1expeven  10836  qsqeqor  10900  fundm2domnop0  11096  ccatrcl1  11178  pfxsuff1eqwrdeq  11267  wrdind  11290  wrd2ind  11291  swrdccat3blem  11307  caucvgrelemcau  11528  rexico  11769  fisumss  11940  fsum2dlemstep  11982  ntrivcvgap  12096  fprodssdc  12138  fprod2dlemstep  12170  0dvds  12359  alzdvds  12402  opoe  12443  omoe  12444  opeo  12445  omeo  12446  m1exp1  12449  nn0enne  12450  nn0o1gt2  12453  gcdneg  12540  dfgcd2  12572  algcvgblem  12608  algcvga  12610  eucalglt  12616  coprmdvds  12651  divgcdcoprmex  12661  cncongr1  12662  prm2orodd  12685  prm23lt5  12823  pockthi  12918  f1ocpbl  13381  f1ovscpbl  13382  f1olecpbl  13383  ismnddef  13488  lmodfopnelem1  14325  tg2  14771  tgcl  14775  neii1  14858  neii2  14860  txlm  14990  reopnap  15257  tgioo  15265  addcncntoplem  15272  gausslemma2dlem0i  15773  2lgslem2  15808  2lgs  15820  2lgsoddprmlem3  15827  uhgr0vb  15921  umgredg  15980  uspgrushgr  16015  uspgrupgr  16016  usgruspgr  16018  uhgr2edg  16041  edg0usgr  16082  vtxdg0v  16096  wlkpropg  16112  wlkv  16114  wlkvg  16116  wlkvtxeledgg  16132  wlkl1loop  16146  upgrwlkedg  16149  upgrwlkvtxedg  16152  uspgr2wlkeq  16153  wlkv0  16157  clwwlkccat  16186  clwwlknp  16202  clwwlkext2edg  16207  bj-elssuniab  16297  bj-nn0sucALT  16483  triap  16543