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  1652  ax11i  1736  equveli  1781  eupickbi  2135  nfabdw  2366  rgen2a  2559  reu6  2961  sseq0  3501  disjel  3514  preq12b  3810  prel12  3811  prneimg  3814  elinti  3893  exmidundif  4249  opthreg  4603  elreldm  4903  issref  5064  relcnvtr  5201  relresfld  5211  funopg  5304  funimass2  5351  f0dom0  5468  fvimacnv  5694  funopdmsn  5763  elunirn  5834  oprabid  5975  op1steq  6264  f1o2ndf1  6313  reldmtpos  6338  rntpos  6342  nntri3or  6578  nnaordex  6613  nnawordex  6614  findcard2  6985  findcard2s  6986  mkvprop  7259  cc2lem  7377  lt2addnq  7516  lt2mulnq  7517  genpelvl  7624  genpelvu  7625  distrlem5prl  7698  distrlem5pru  7699  caucvgprlemnkj  7778  map2psrprg  7917  rereceu  8001  ltxrlt  8137  0mnnnnn0  9326  elnnnn0b  9338  nn0le2is012  9454  btwnz  9491  uz11  9670  nn01to3  9737  zq  9746  xrltso  9917  xltnegi  9956  xnn0lenn0nn0  9986  xnn0xadd0  9988  iccleub  10052  fzdcel  10161  uznfz  10224  2ffzeq  10262  elfzonlteqm1  10337  icogelb  10406  flqeqceilz  10461  modqadd1  10504  modqmul1  10520  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  fzfig  10573  seqf1og  10664  m1expeven  10729  qsqeqor  10793  fundm2domnop0  10988  caucvgrelemcau  11262  rexico  11503  fisumss  11674  fsum2dlemstep  11716  ntrivcvgap  11830  fprodssdc  11872  fprod2dlemstep  11904  0dvds  12093  alzdvds  12136  opoe  12177  omoe  12178  opeo  12179  omeo  12180  m1exp1  12183  nn0enne  12184  nn0o1gt2  12187  gcdneg  12274  dfgcd2  12306  algcvgblem  12342  algcvga  12344  eucalglt  12350  coprmdvds  12385  divgcdcoprmex  12395  cncongr1  12396  prm2orodd  12419  prm23lt5  12557  pockthi  12652  f1ocpbl  13114  f1ovscpbl  13115  f1olecpbl  13116  ismnddef  13221  lmodfopnelem1  14057  tg2  14503  tgcl  14507  neii1  14590  neii2  14592  txlm  14722  reopnap  14989  tgioo  14997  addcncntoplem  15004  gausslemma2dlem0i  15505  2lgslem2  15540  2lgs  15552  2lgsoddprmlem3  15559  bj-elssuniab  15689  bj-nn0sucALT  15876  triap  15930