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  1676  ax11i  1760  equveli  1805  eupickbi  2160  nfabdw  2391  rgen2a  2584  reu6  2992  sseq0  3533  disjel  3546  preq12b  3847  prel12  3848  prneimg  3851  elinti  3931  exmidundif  4289  opthreg  4647  elreldm  4949  issref  5110  relcnvtr  5247  relresfld  5257  funopg  5351  funimass2  5398  f0dom0  5518  fvimacnv  5749  funopdmsn  5818  elunirn  5889  oprabid  6032  op1steq  6323  f1o2ndf1  6372  reldmtpos  6397  rntpos  6401  nntri3or  6637  nnaordex  6672  nnawordex  6673  findcard2  7047  findcard2s  7048  mkvprop  7321  cc2lem  7448  lt2addnq  7587  lt2mulnq  7588  genpelvl  7695  genpelvu  7696  distrlem5prl  7769  distrlem5pru  7770  caucvgprlemnkj  7849  map2psrprg  7988  rereceu  8072  ltxrlt  8208  0mnnnnn0  9397  elnnnn0b  9409  nn0le2is012  9525  btwnz  9562  uz11  9741  nn01to3  9808  zq  9817  xrltso  9988  xltnegi  10027  xnn0lenn0nn0  10057  xnn0xadd0  10059  iccleub  10123  fzdcel  10232  uznfz  10295  2ffzeq  10333  elfzonlteqm1  10411  icogelb  10480  flqeqceilz  10535  modqadd1  10578  modqmul1  10594  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  fzfig  10647  seqf1og  10738  m1expeven  10803  qsqeqor  10867  fundm2domnop0  11062  pfxsuff1eqwrdeq  11226  wrdind  11249  wrd2ind  11250  swrdccat3blem  11266  caucvgrelemcau  11486  rexico  11727  fisumss  11898  fsum2dlemstep  11940  ntrivcvgap  12054  fprodssdc  12096  fprod2dlemstep  12128  0dvds  12317  alzdvds  12360  opoe  12401  omoe  12402  opeo  12403  omeo  12404  m1exp1  12407  nn0enne  12408  nn0o1gt2  12411  gcdneg  12498  dfgcd2  12530  algcvgblem  12566  algcvga  12568  eucalglt  12574  coprmdvds  12609  divgcdcoprmex  12619  cncongr1  12620  prm2orodd  12643  prm23lt5  12781  pockthi  12876  f1ocpbl  13339  f1ovscpbl  13340  f1olecpbl  13341  ismnddef  13446  lmodfopnelem1  14282  tg2  14728  tgcl  14732  neii1  14815  neii2  14817  txlm  14947  reopnap  15214  tgioo  15222  addcncntoplem  15229  gausslemma2dlem0i  15730  2lgslem2  15765  2lgs  15777  2lgsoddprmlem3  15784  uhgr0vb  15878  umgredg  15937  uspgrushgr  15972  uspgrupgr  15973  usgruspgr  15975  uhgr2edg  15998  wlkpropg  16030  wlkvg  16031  wlkvtxeledgg  16041  bj-elssuniab  16113  bj-nn0sucALT  16299  triap  16356