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  1654  ax11i  1738  equveli  1783  eupickbi  2138  nfabdw  2369  rgen2a  2562  reu6  2969  sseq0  3510  disjel  3523  preq12b  3824  prel12  3825  prneimg  3828  elinti  3908  exmidundif  4266  opthreg  4622  elreldm  4923  issref  5084  relcnvtr  5221  relresfld  5231  funopg  5324  funimass2  5371  f0dom0  5491  fvimacnv  5718  funopdmsn  5787  elunirn  5858  oprabid  5999  op1steq  6288  f1o2ndf1  6337  reldmtpos  6362  rntpos  6366  nntri3or  6602  nnaordex  6637  nnawordex  6638  findcard2  7012  findcard2s  7013  mkvprop  7286  cc2lem  7413  lt2addnq  7552  lt2mulnq  7553  genpelvl  7660  genpelvu  7661  distrlem5prl  7734  distrlem5pru  7735  caucvgprlemnkj  7814  map2psrprg  7953  rereceu  8037  ltxrlt  8173  0mnnnnn0  9362  elnnnn0b  9374  nn0le2is012  9490  btwnz  9527  uz11  9706  nn01to3  9773  zq  9782  xrltso  9953  xltnegi  9992  xnn0lenn0nn0  10022  xnn0xadd0  10024  iccleub  10088  fzdcel  10197  uznfz  10260  2ffzeq  10298  elfzonlteqm1  10376  icogelb  10445  flqeqceilz  10500  modqadd1  10543  modqmul1  10559  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  fzfig  10612  seqf1og  10703  m1expeven  10768  qsqeqor  10832  fundm2domnop0  11027  pfxsuff1eqwrdeq  11190  wrdind  11213  wrd2ind  11214  swrdccat3blem  11230  caucvgrelemcau  11406  rexico  11647  fisumss  11818  fsum2dlemstep  11860  ntrivcvgap  11974  fprodssdc  12016  fprod2dlemstep  12048  0dvds  12237  alzdvds  12280  opoe  12321  omoe  12322  opeo  12323  omeo  12324  m1exp1  12327  nn0enne  12328  nn0o1gt2  12331  gcdneg  12418  dfgcd2  12450  algcvgblem  12486  algcvga  12488  eucalglt  12494  coprmdvds  12529  divgcdcoprmex  12539  cncongr1  12540  prm2orodd  12563  prm23lt5  12701  pockthi  12796  f1ocpbl  13258  f1ovscpbl  13259  f1olecpbl  13260  ismnddef  13365  lmodfopnelem1  14201  tg2  14647  tgcl  14651  neii1  14734  neii2  14736  txlm  14866  reopnap  15133  tgioo  15141  addcncntoplem  15148  gausslemma2dlem0i  15649  2lgslem2  15684  2lgs  15696  2lgsoddprmlem3  15703  uhgr0vb  15795  umgredg  15849  bj-elssuniab  15927  bj-nn0sucALT  16113  triap  16170