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  2992  sseq0  3533  disjel  3546  preq12b  3848  prel12  3849  prneimg  3852  elinti  3932  exmidundif  4290  opthreg  4648  elreldm  4950  issref  5111  relcnvtr  5248  relresfld  5258  funopg  5352  funimass2  5399  f0dom0  5521  fvimacnv  5752  funopdmsn  5823  elunirn  5896  oprabid  6039  op1steq  6331  f1o2ndf1  6380  reldmtpos  6405  rntpos  6409  nntri3or  6647  nnaordex  6682  nnawordex  6683  findcard2  7059  findcard2s  7060  mkvprop  7336  cc2lem  7463  lt2addnq  7602  lt2mulnq  7603  genpelvl  7710  genpelvu  7711  distrlem5prl  7784  distrlem5pru  7785  caucvgprlemnkj  7864  map2psrprg  8003  rereceu  8087  ltxrlt  8223  0mnnnnn0  9412  elnnnn0b  9424  nn0le2is012  9540  btwnz  9577  uz11  9757  nn01to3  9824  zq  9833  xrltso  10004  xltnegi  10043  xnn0lenn0nn0  10073  xnn0xadd0  10075  iccleub  10139  fzdcel  10248  uznfz  10311  2ffzeq  10349  elfzonlteqm1  10428  icogelb  10497  flqeqceilz  10552  modqadd1  10595  modqmul1  10611  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  fzfig  10664  seqf1og  10755  m1expeven  10820  qsqeqor  10884  fundm2domnop0  11080  ccatrcl1  11162  pfxsuff1eqwrdeq  11247  wrdind  11270  wrd2ind  11271  swrdccat3blem  11287  caucvgrelemcau  11507  rexico  11748  fisumss  11919  fsum2dlemstep  11961  ntrivcvgap  12075  fprodssdc  12117  fprod2dlemstep  12149  0dvds  12338  alzdvds  12381  opoe  12422  omoe  12423  opeo  12424  omeo  12425  m1exp1  12428  nn0enne  12429  nn0o1gt2  12432  gcdneg  12519  dfgcd2  12551  algcvgblem  12587  algcvga  12589  eucalglt  12595  coprmdvds  12630  divgcdcoprmex  12640  cncongr1  12641  prm2orodd  12664  prm23lt5  12802  pockthi  12897  f1ocpbl  13360  f1ovscpbl  13361  f1olecpbl  13362  ismnddef  13467  lmodfopnelem1  14304  tg2  14750  tgcl  14754  neii1  14837  neii2  14839  txlm  14969  reopnap  15236  tgioo  15244  addcncntoplem  15251  gausslemma2dlem0i  15752  2lgslem2  15787  2lgs  15799  2lgsoddprmlem3  15806  uhgr0vb  15900  umgredg  15959  uspgrushgr  15994  uspgrupgr  15995  usgruspgr  15997  uhgr2edg  16020  vtxdg0v  16054  wlkpropg  16070  wlkv  16072  wlkvg  16074  wlkvtxeledgg  16090  wlkl1loop  16104  upgrwlkedg  16107  upgrwlkvtxedg  16110  uspgr2wlkeq  16111  wlkv0  16115  clwwlkccat  16144  clwwlknp  16159  clwwlkext2edg  16164  bj-elssuniab  16238  bj-nn0sucALT  16424  triap  16485