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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  19.33bdc  1683  ax11i  1766  equveli  1812  eupickbi  2169  nfabdw  2411  rgen2a  2604  reu6  3015  disjel  3579  preq12b  3895  prel12  3896  prneimg  3899  elinti  3979  exmidundif  4343  opthreg  4703  elreldm  5008  issref  5170  relcnvtr  5307  relresfld  5317  funopg  5411  funimass2  5459  f0dom0  5586  fvimacnv  5824  funopdmsn  5895  elunirn  5972  oprabid  6117  op1steq  6413  f1o2ndf1  6464  fvn0elsuppb  6492  suppfnss  6497  reldmtpos  6524  rntpos  6528  nntri3or  6766  nnaordex  6801  nnawordex  6802  findcard2  7193  findcard2s  7194  mkvprop  7498  cc2lem  7632  lt2addnq  7771  lt2mulnq  7772  genpelvl  7879  genpelvu  7880  distrlem5prl  7953  distrlem5pru  7954  caucvgprlemnkj  8033  map2psrprg  8172  rereceu  8256  ltxrlt  8391  0mnnnnn0  9595  elnnnn0b  9607  nn0le2is012  9728  btwnz  9765  uz11  9945  nn01to3  10017  zq  10026  xrltso  10198  xltnegi  10237  xnn0lenn0nn0  10267  xnn0xadd0  10269  iccleub  10333  fzdcel  10444  uznfz  10510  2ffzeq  10548  elfzonlteqm1  10628  icogelb  10700  flqeqceilz  10755  modqadd1  10798  modqmul1  10814  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  fzfig  10867  seqf1og  10958  m1expeven  11023  qsqeqor  11087  hashf1lem2  11286  fundm2domnop0  11300  ccatrcl1  11382  pfxsuff1eqwrdeq  11471  wrdind  11494  wrd2ind  11495  swrdccat3blem  11511  caucvgrelemcau  11746  rexico  11987  fisumss  12159  fsum2dlemstep  12201  ntrivcvgap  12315  fprodssdc  12357  fprod2dlemstep  12389  0dvds  12578  alzdvds  12621  opoe  12662  omoe  12663  opeo  12664  omeo  12665  m1exp1  12668  nn0enne  12669  nn0o1gt2  12672  gcdneg  12759  dfgcd2  12791  algcvgblem  12827  algcvga  12829  eucalglt  12835  coprmdvds  12870  divgcdcoprmex  12880  cncongr1  12881  prm2orodd  12904  prm23lt5  13042  pockthi  13137  ballotfilemfc0  13232  ballotfilemfcc  13233  f1ocpbl  13632  f1ovscpbl  13633  f1olecpbl  13634  ismnddef  13731  lmodfopnelem1  14661  tg2  15161  tgcl  15165  neii1  15248  neii2  15250  txlm  15380  reopnap  15647  tgioo  15655  addcncntoplem  15662  birthdaylem1g  16087  gausslemma2dlem0i  16176  2lgslem2  16211  2lgs  16223  2lgsoddprmlem3  16230  uhgr0vb  16325  umgredg  16386  uspgrushgr  16421  uspgrupgr  16422  usgruspgr  16424  uhgr2edg  16447  edg0usgr  16488  egrsubgr  16504  0uhgrsubgr  16506  uhgrspansubgrlem  16517  vtxdg0v  16535  wlkpropg  16565  wlkv  16567  wlkvg  16569  wlkvtxeledgg  16585  wlkl1loop  16599  upgrwlkedg  16602  upgrwlkvtxedg  16605  uspgr2wlkeq  16606  wlkv0  16610  clwwlkccat  16642  clwwlknp  16658  clwwlkext2edg  16663  eupth2lem3lem4fi  16714  bj-elssuniab  16819  bj-nn0sucALT  17004  triap  17078