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  2950  sseq0  3489  disjel  3502  preq12b  3797  prel12  3798  prneimg  3801  elinti  3880  exmidundif  4236  opthreg  4589  elreldm  4889  issref  5049  relcnvtr  5186  relresfld  5196  funopg  5289  funimass2  5333  f0dom0  5448  fvimacnv  5674  elunirn  5810  oprabid  5951  op1steq  6234  f1o2ndf1  6283  reldmtpos  6308  rntpos  6312  nntri3or  6548  nnaordex  6583  nnawordex  6584  findcard2  6947  findcard2s  6948  mkvprop  7219  cc2lem  7328  lt2addnq  7466  lt2mulnq  7467  genpelvl  7574  genpelvu  7575  distrlem5prl  7648  distrlem5pru  7649  caucvgprlemnkj  7728  map2psrprg  7867  rereceu  7951  ltxrlt  8087  0mnnnnn0  9275  elnnnn0b  9287  nn0le2is012  9402  btwnz  9439  uz11  9618  nn01to3  9685  zq  9694  xrltso  9865  xltnegi  9904  xnn0lenn0nn0  9934  xnn0xadd0  9936  iccleub  10000  fzdcel  10109  uznfz  10172  2ffzeq  10210  elfzonlteqm1  10280  icogelb  10337  flqeqceilz  10392  modqadd1  10435  modqmul1  10451  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  fzfig  10504  seqf1og  10595  m1expeven  10660  qsqeqor  10724  caucvgrelemcau  11127  rexico  11368  fisumss  11538  fsum2dlemstep  11580  ntrivcvgap  11694  fprodssdc  11736  fprod2dlemstep  11768  0dvds  11957  alzdvds  11999  opoe  12039  omoe  12040  opeo  12041  omeo  12042  m1exp1  12045  nn0enne  12046  nn0o1gt2  12049  gcdneg  12122  dfgcd2  12154  algcvgblem  12190  algcvga  12192  eucalglt  12198  coprmdvds  12233  divgcdcoprmex  12243  cncongr1  12244  prm2orodd  12267  prm23lt5  12404  pockthi  12499  f1ocpbl  12897  f1ovscpbl  12898  f1olecpbl  12899  ismnddef  13002  lmodfopnelem1  13823  tg2  14239  tgcl  14243  neii1  14326  neii2  14328  txlm  14458  reopnap  14725  tgioo  14733  addcncntoplem  14740  gausslemma2dlem0i  15214  2lgslem2  15249  2lgs  15261  2lgsoddprmlem3  15268  bj-elssuniab  15353  bj-nn0sucALT  15540  triap  15589