Theorem biimtrdi 163

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
biimtrdi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
biimtrdi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
biimtrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrdi

Step	Hyp	Ref	Expression
1		biimtrdi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  1640  ax11i  1724  equveli  1769  eupickbi  2118  nfabdw  2348  rgen2a  2541  reu6  2938  sseq0  3476  disjel  3489  preq12b  3782  prel12  3783  prneimg  3786  elinti  3865  exmidundif  4218  opthreg  4567  elreldm  4865  issref  5023  relcnvtr  5160  relresfld  5170  funopg  5262  funimass2  5306  f0dom0  5421  fvimacnv  5644  elunirn  5780  oprabid  5920  op1steq  6194  f1o2ndf1  6243  reldmtpos  6268  rntpos  6272  nntri3or  6508  nnaordex  6543  nnawordex  6544  findcard2  6903  findcard2s  6904  mkvprop  7170  cc2lem  7279  lt2addnq  7417  lt2mulnq  7418  genpelvl  7525  genpelvu  7526  distrlem5prl  7599  distrlem5pru  7600  caucvgprlemnkj  7679  map2psrprg  7818  rereceu  7902  ltxrlt  8037  0mnnnnn0  9222  elnnnn0b  9234  nn0le2is012  9349  btwnz  9386  uz11  9564  nn01to3  9631  zq  9640  xrltso  9810  xltnegi  9849  xnn0lenn0nn0  9879  xnn0xadd0  9881  iccleub  9945  fzdcel  10054  uznfz  10117  2ffzeq  10155  elfzonlteqm1  10224  icogelb  10280  flqeqceilz  10332  modqadd1  10375  modqmul1  10391  frecuzrdgtcl  10426  frecuzrdgfunlem  10433  fzfig  10444  m1expeven  10581  qsqeqor  10645  caucvgrelemcau  11003  rexico  11244  fisumss  11414  fsum2dlemstep  11456  ntrivcvgap  11570  fprodssdc  11612  fprod2dlemstep  11644  0dvds  11832  alzdvds  11874  opoe  11914  omoe  11915  opeo  11916  omeo  11917  m1exp1  11920  nn0enne  11921  nn0o1gt2  11924  gcdneg  11997  dfgcd2  12029  algcvgblem  12063  algcvga  12065  eucalglt  12071  coprmdvds  12106  divgcdcoprmex  12116  cncongr1  12117  prm2orodd  12140  prm23lt5  12277  pockthi  12370  f1ocpbl  12750  f1ovscpbl  12751  f1olecpbl  12752  ismnddef  12841  lmodfopnelem1  13513  tg2  13856  tgcl  13860  neii1  13943  neii2  13945  txlm  14075  reopnap  14334  tgioo  14342  addcncntoplem  14347  2lgsoddprmlem3  14755  bj-elssuniab  14839  bj-nn0sucALT  15026  triap  15074