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  1653  ax11i  1737  equveli  1782  eupickbi  2136  nfabdw  2367  rgen2a  2560  reu6  2962  sseq0  3502  disjel  3515  preq12b  3811  prel12  3812  prneimg  3815  elinti  3894  exmidundif  4250  opthreg  4604  elreldm  4904  issref  5065  relcnvtr  5202  relresfld  5212  funopg  5305  funimass2  5352  f0dom0  5469  fvimacnv  5695  funopdmsn  5764  elunirn  5835  oprabid  5976  op1steq  6265  f1o2ndf1  6314  reldmtpos  6339  rntpos  6343  nntri3or  6579  nnaordex  6614  nnawordex  6615  findcard2  6986  findcard2s  6987  mkvprop  7260  cc2lem  7378  lt2addnq  7517  lt2mulnq  7518  genpelvl  7625  genpelvu  7626  distrlem5prl  7699  distrlem5pru  7700  caucvgprlemnkj  7779  map2psrprg  7918  rereceu  8002  ltxrlt  8138  0mnnnnn0  9327  elnnnn0b  9339  nn0le2is012  9455  btwnz  9492  uz11  9671  nn01to3  9738  zq  9747  xrltso  9918  xltnegi  9957  xnn0lenn0nn0  9987  xnn0xadd0  9989  iccleub  10053  fzdcel  10162  uznfz  10225  2ffzeq  10263  elfzonlteqm1  10339  icogelb  10408  flqeqceilz  10463  modqadd1  10506  modqmul1  10522  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  fzfig  10575  seqf1og  10666  m1expeven  10731  qsqeqor  10795  fundm2domnop0  10990  caucvgrelemcau  11291  rexico  11532  fisumss  11703  fsum2dlemstep  11745  ntrivcvgap  11859  fprodssdc  11901  fprod2dlemstep  11933  0dvds  12122  alzdvds  12165  opoe  12206  omoe  12207  opeo  12208  omeo  12209  m1exp1  12212  nn0enne  12213  nn0o1gt2  12216  gcdneg  12303  dfgcd2  12335  algcvgblem  12371  algcvga  12373  eucalglt  12379  coprmdvds  12414  divgcdcoprmex  12424  cncongr1  12425  prm2orodd  12448  prm23lt5  12586  pockthi  12681  f1ocpbl  13143  f1ovscpbl  13144  f1olecpbl  13145  ismnddef  13250  lmodfopnelem1  14086  tg2  14532  tgcl  14536  neii1  14619  neii2  14621  txlm  14751  reopnap  15018  tgioo  15026  addcncntoplem  15033  gausslemma2dlem0i  15534  2lgslem2  15569  2lgs  15581  2lgsoddprmlem3  15588  bj-elssuniab  15727  bj-nn0sucALT  15914  triap  15968