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  1683  ax11i  1766  equveli  1812  eupickbi  2169  nfabdw  2411  rgen2a  2604  reu6  3015  sseq0  3564  disjel  3578  preq12b  3890  prel12  3891  prneimg  3894  elinti  3974  exmidundif  4338  opthreg  4698  elreldm  5003  issref  5165  relcnvtr  5302  relresfld  5312  funopg  5406  funimass2  5454  f0dom0  5581  fvimacnv  5815  funopdmsn  5886  elunirn  5962  oprabid  6107  op1steq  6403  f1o2ndf1  6454  fvn0elsuppb  6482  suppfnss  6487  reldmtpos  6514  rntpos  6518  nntri3or  6756  nnaordex  6791  nnawordex  6792  findcard2  7183  findcard2s  7184  mkvprop  7488  cc2lem  7622  lt2addnq  7761  lt2mulnq  7762  genpelvl  7869  genpelvu  7870  distrlem5prl  7943  distrlem5pru  7944  caucvgprlemnkj  8023  map2psrprg  8162  rereceu  8246  ltxrlt  8381  0mnnnnn0  9574  elnnnn0b  9586  nn0le2is012  9707  btwnz  9744  uz11  9924  nn01to3  9996  zq  10005  xrltso  10177  xltnegi  10216  xnn0lenn0nn0  10246  xnn0xadd0  10248  iccleub  10312  fzdcel  10423  uznfz  10488  2ffzeq  10526  elfzonlteqm1  10606  icogelb  10678  flqeqceilz  10733  modqadd1  10776  modqmul1  10792  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  fzfig  10845  seqf1og  10936  m1expeven  11001  qsqeqor  11065  hashf1lem2  11264  fundm2domnop0  11278  ccatrcl1  11360  pfxsuff1eqwrdeq  11449  wrdind  11472  wrd2ind  11473  swrdccat3blem  11489  caucvgrelemcau  11724  rexico  11965  fisumss  12137  fsum2dlemstep  12179  ntrivcvgap  12293  fprodssdc  12335  fprod2dlemstep  12367  0dvds  12556  alzdvds  12599  opoe  12640  omoe  12641  opeo  12642  omeo  12643  m1exp1  12646  nn0enne  12647  nn0o1gt2  12650  gcdneg  12737  dfgcd2  12769  algcvgblem  12805  algcvga  12807  eucalglt  12813  coprmdvds  12848  divgcdcoprmex  12858  cncongr1  12859  prm2orodd  12882  prm23lt5  13020  pockthi  13115  ballotfilemfc0  13210  ballotfilemfcc  13211  f1ocpbl  13609  f1ovscpbl  13610  f1olecpbl  13611  ismnddef  13708  lmodfopnelem1  14633  tg2  15084  tgcl  15088  neii1  15171  neii2  15173  txlm  15303  reopnap  15570  tgioo  15578  addcncntoplem  15585  gausslemma2dlem0i  16090  2lgslem2  16125  2lgs  16137  2lgsoddprmlem3  16144  uhgr0vb  16239  umgredg  16300  uspgrushgr  16335  uspgrupgr  16336  usgruspgr  16338  uhgr2edg  16361  edg0usgr  16402  egrsubgr  16418  0uhgrsubgr  16420  uhgrspansubgrlem  16431  vtxdg0v  16449  wlkpropg  16479  wlkv  16481  wlkvg  16483  wlkvtxeledgg  16499  wlkl1loop  16513  upgrwlkedg  16516  upgrwlkvtxedg  16519  uspgr2wlkeq  16520  wlkv0  16524  clwwlkccat  16556  clwwlknp  16572  clwwlkext2edg  16577  eupth2lem3lem4fi  16628  bj-elssuniab  16733  bj-nn0sucALT  16918  triap  16983