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  7499  cc2lem  7633  lt2addnq  7772  lt2mulnq  7773  genpelvl  7880  genpelvu  7881  distrlem5prl  7954  distrlem5pru  7955  caucvgprlemnkj  8034  map2psrprg  8173  rereceu  8257  ltxrlt  8392  0mnnnnn0  9600  elnnnn0b  9612  nn0le2is012  9733  btwnz  9770  uz11  9955  nn01to3  10027  zq  10036  xrltso  10209  xltnegi  10248  xnn0lenn0nn0  10278  xnn0xadd0  10280  iccleub  10344  fzdcel  10455  uznfz  10521  2ffzeq  10559  elfzonlteqm1  10639  icogelb  10711  flqeqceilz  10770  modqadd1  10813  modqmul1  10829  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  fzfig  10882  seqf1og  10973  m1expeven  11038  qsqeqor  11102  hashf1lem2  11302  fundm2domnop0  11316  ccatrcl1  11398  pfxsuff1eqwrdeq  11487  wrdind  11510  wrd2ind  11511  swrdccat3blem  11527  caucvgrelemcau  11762  rexico  12004  fisumss  12178  fsum2dlemstep  12220  ntrivcvgap  12334  fprodssdc  12376  fprod2dlemstep  12408  0dvds  12597  alzdvds  12640  opoe  12681  omoe  12682  opeo  12683  omeo  12684  m1exp1  12687  nn0enne  12688  nn0o1gt2  12691  gcdneg  12778  dfgcd2  12810  algcvgblem  12846  algcvga  12848  eucalglt  12854  coprmdvds  12889  divgcdcoprmex  12899  cncongr1  12900  prm2orodd  12923  prm23lt5  13065  pockthi  13160  ballotfilemfc0  13284  ballotfilemfcc  13285  f1ocpbl  13685  f1ovscpbl  13686  f1olecpbl  13687  ismnddef  13784  lmodfopnelem1  14745  tg2  15252  tgcl  15256  neii1  15339  neii2  15341  txlm  15471  reopnap  15738  tgioo  15746  addcncntoplem  15753  birthdaylem1g  16186  gausslemma2dlem0i  16342  2lgslem2  16377  2lgs  16389  2lgsoddprmlem3  16396  uhgr0vb  16491  umgredg  16552  uspgrushgr  16587  uspgrupgr  16588  usgruspgr  16590  uhgr2edg  16613  edg0usgr  16654  egrsubgr  16670  0uhgrsubgr  16672  uhgrspansubgrlem  16683  vtxdg0v  16701  wlkpropg  16731  wlkv  16733  wlkvg  16735  wlkvtxeledgg  16751  wlkl1loop  16765  upgrwlkedg  16768  upgrwlkvtxedg  16771  uspgr2wlkeq  16772  wlkv0  16776  clwwlkccat  16808  clwwlknp  16824  clwwlkext2edg  16829  eupth2lem3lem4fi  16880  bj-elssuniab  16985  bj-nn0sucALT  17170  triap  17244