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  1644  ax11i  1728  equveli  1773  eupickbi  2127  nfabdw  2358  rgen2a  2551  reu6  2953  sseq0  3493  disjel  3506  preq12b  3801  prel12  3802  prneimg  3805  elinti  3884  exmidundif  4240  opthreg  4593  elreldm  4893  issref  5053  relcnvtr  5190  relresfld  5200  funopg  5293  funimass2  5337  f0dom0  5452  fvimacnv  5678  elunirn  5814  oprabid  5955  op1steq  6238  f1o2ndf1  6287  reldmtpos  6312  rntpos  6316  nntri3or  6552  nnaordex  6587  nnawordex  6588  findcard2  6951  findcard2s  6952  mkvprop  7225  cc2lem  7335  lt2addnq  7473  lt2mulnq  7474  genpelvl  7581  genpelvu  7582  distrlem5prl  7655  distrlem5pru  7656  caucvgprlemnkj  7735  map2psrprg  7874  rereceu  7958  ltxrlt  8094  0mnnnnn0  9283  elnnnn0b  9295  nn0le2is012  9410  btwnz  9447  uz11  9626  nn01to3  9693  zq  9702  xrltso  9873  xltnegi  9912  xnn0lenn0nn0  9942  xnn0xadd0  9944  iccleub  10008  fzdcel  10117  uznfz  10180  2ffzeq  10218  elfzonlteqm1  10288  icogelb  10357  flqeqceilz  10412  modqadd1  10455  modqmul1  10471  frecuzrdgtcl  10506  frecuzrdgfunlem  10513  fzfig  10524  seqf1og  10615  m1expeven  10680  qsqeqor  10744  caucvgrelemcau  11147  rexico  11388  fisumss  11559  fsum2dlemstep  11601  ntrivcvgap  11715  fprodssdc  11757  fprod2dlemstep  11789  0dvds  11978  alzdvds  12021  opoe  12062  omoe  12063  opeo  12064  omeo  12065  m1exp1  12068  nn0enne  12069  nn0o1gt2  12072  gcdneg  12159  dfgcd2  12191  algcvgblem  12227  algcvga  12229  eucalglt  12235  coprmdvds  12270  divgcdcoprmex  12280  cncongr1  12281  prm2orodd  12304  prm23lt5  12442  pockthi  12537  f1ocpbl  12964  f1ovscpbl  12965  f1olecpbl  12966  ismnddef  13069  lmodfopnelem1  13890  tg2  14306  tgcl  14310  neii1  14393  neii2  14395  txlm  14525  reopnap  14792  tgioo  14800  addcncntoplem  14807  gausslemma2dlem0i  15308  2lgslem2  15343  2lgs  15355  2lgsoddprmlem3  15362  bj-elssuniab  15447  bj-nn0sucALT  15634  triap  15683