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  5454  fvimacnv  5680  elunirn  5816  oprabid  5957  op1steq  6246  f1o2ndf1  6295  reldmtpos  6320  rntpos  6324  nntri3or  6560  nnaordex  6595  nnawordex  6596  findcard2  6959  findcard2s  6960  mkvprop  7233  cc2lem  7351  lt2addnq  7490  lt2mulnq  7491  genpelvl  7598  genpelvu  7599  distrlem5prl  7672  distrlem5pru  7673  caucvgprlemnkj  7752  map2psrprg  7891  rereceu  7975  ltxrlt  8111  0mnnnnn0  9300  elnnnn0b  9312  nn0le2is012  9427  btwnz  9464  uz11  9643  nn01to3  9710  zq  9719  xrltso  9890  xltnegi  9929  xnn0lenn0nn0  9959  xnn0xadd0  9961  iccleub  10025  fzdcel  10134  uznfz  10197  2ffzeq  10235  elfzonlteqm1  10305  icogelb  10374  flqeqceilz  10429  modqadd1  10472  modqmul1  10488  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  fzfig  10541  seqf1og  10632  m1expeven  10697  qsqeqor  10761  caucvgrelemcau  11164  rexico  11405  fisumss  11576  fsum2dlemstep  11618  ntrivcvgap  11732  fprodssdc  11774  fprod2dlemstep  11806  0dvds  11995  alzdvds  12038  opoe  12079  omoe  12080  opeo  12081  omeo  12082  m1exp1  12085  nn0enne  12086  nn0o1gt2  12089  gcdneg  12176  dfgcd2  12208  algcvgblem  12244  algcvga  12246  eucalglt  12252  coprmdvds  12287  divgcdcoprmex  12297  cncongr1  12298  prm2orodd  12321  prm23lt5  12459  pockthi  12554  f1ocpbl  13015  f1ovscpbl  13016  f1olecpbl  13017  ismnddef  13122  lmodfopnelem1  13958  tg2  14404  tgcl  14408  neii1  14491  neii2  14493  txlm  14623  reopnap  14890  tgioo  14898  addcncntoplem  14905  gausslemma2dlem0i  15406  2lgslem2  15441  2lgs  15453  2lgsoddprmlem3  15460  bj-elssuniab  15545  bj-nn0sucALT  15732  triap  15786