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  1630  ax11i  1714  equveli  1759  eupickbi  2108  nfabdw  2338  rgen2a  2531  reu6  2928  sseq0  3466  disjel  3479  preq12b  3772  prel12  3773  prneimg  3776  elinti  3855  exmidundif  4208  opthreg  4557  elreldm  4855  issref  5013  relcnvtr  5150  relresfld  5160  funopg  5252  funimass2  5296  f0dom0  5411  fvimacnv  5634  elunirn  5770  oprabid  5910  op1steq  6183  f1o2ndf1  6232  reldmtpos  6257  rntpos  6261  nntri3or  6497  nnaordex  6532  nnawordex  6533  findcard2  6892  findcard2s  6893  mkvprop  7159  cc2lem  7268  lt2addnq  7406  lt2mulnq  7407  genpelvl  7514  genpelvu  7515  distrlem5prl  7588  distrlem5pru  7589  caucvgprlemnkj  7668  map2psrprg  7807  rereceu  7891  ltxrlt  8026  0mnnnnn0  9211  elnnnn0b  9223  nn0le2is012  9338  btwnz  9375  uz11  9553  nn01to3  9620  zq  9629  xrltso  9799  xltnegi  9838  xnn0lenn0nn0  9868  xnn0xadd0  9870  iccleub  9934  fzdcel  10043  uznfz  10106  2ffzeq  10144  elfzonlteqm1  10213  icogelb  10269  flqeqceilz  10321  modqadd1  10364  modqmul1  10380  frecuzrdgtcl  10415  frecuzrdgfunlem  10422  fzfig  10433  m1expeven  10570  qsqeqor  10634  caucvgrelemcau  10992  rexico  11233  fisumss  11403  fsum2dlemstep  11445  ntrivcvgap  11559  fprodssdc  11601  fprod2dlemstep  11633  0dvds  11821  alzdvds  11863  opoe  11903  omoe  11904  opeo  11905  omeo  11906  m1exp1  11909  nn0enne  11910  nn0o1gt2  11913  gcdneg  11986  dfgcd2  12018  algcvgblem  12052  algcvga  12054  eucalglt  12060  coprmdvds  12095  divgcdcoprmex  12105  cncongr1  12106  prm2orodd  12129  prm23lt5  12266  pockthi  12359  f1ocpbl  12738  f1ovscpbl  12739  f1olecpbl  12740  ismnddef  12825  lmodfopnelem1  13420  tg2  13700  tgcl  13704  neii1  13787  neii2  13789  txlm  13919  reopnap  14178  tgioo  14186  addcncntoplem  14191  2lgsoddprmlem3  14599  bj-elssuniab  14683  bj-nn0sucALT  14870  triap  14918