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  4345  opthreg  4705  elreldm  5010  issref  5173  relcnvtr  5310  relresfld  5320  funopg  5414  funimass2  5462  f0dom0  5589  fvimacnv  5827  funopdmsn  5898  elunirn  5975  oprabid  6120  op1steq  6417  f1o2ndf1  6468  fvn0elsuppb  6496  suppfnss  6501  reldmtpos  6528  rntpos  6532  nntri3or  6770  nnaordex  6805  nnawordex  6806  findcard2  7197  findcard2s  7198  mkvprop  7504  cc2lem  7638  lt2addnq  7777  lt2mulnq  7778  genpelvl  7885  genpelvu  7886  distrlem5prl  7959  distrlem5pru  7960  caucvgprlemnkj  8039  map2psrprg  8178  rereceu  8262  ltxrlt  8397  0mnnnnn0  9606  elnnnn0b  9618  nn0le2is012  9739  btwnz  9776  uz11  9961  nn01to3  10033  zq  10042  xrltso  10215  xltnegi  10254  xnn0lenn0nn0  10284  xnn0xadd0  10286  iccleub  10350  fzdcel  10461  uznfz  10527  2ffzeq  10565  elfzonlteqm1  10645  icogelb  10717  flqeqceilz  10776  modqadd1  10819  modqmul1  10835  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  fzfig  10888  seqf1og  10979  m1expeven  11044  qsqeqor  11108  hashf1lem2  11308  fundm2domnop0  11322  ccatrcl1  11404  pfxsuff1eqwrdeq  11493  wrdind  11516  wrd2ind  11517  swrdccat3blem  11533  caucvgrelemcau  11768  rexico  12010  fisumss  12184  fsum2dlemstep  12226  ntrivcvgap  12340  fprodssdc  12382  fprod2dlemstep  12414  0dvds  12603  alzdvds  12646  opoe  12687  omoe  12688  opeo  12689  omeo  12690  m1exp1  12693  nn0enne  12694  nn0o1gt2  12697  gcdneg  12784  dfgcd2  12816  algcvgblem  12852  algcvga  12854  eucalglt  12860  coprmdvds  12895  divgcdcoprmex  12905  cncongr1  12906  prm2orodd  12929  prm23lt5  13071  pockthi  13166  ballotfilemfc0  13290  ballotfilemfcc  13291  f1ocpbl  13691  f1ovscpbl  13692  f1olecpbl  13693  ismnddef  13790  lmodfopnelem1  14770  tg2  15286  tgcl  15290  neii1  15373  neii2  15375  txlm  15505  reopnap  15772  tgioo  15780  addcncntoplem  15787  sineq0re  16076  birthdaylem1g  16225  gausslemma2dlem0i  16381  2lgslem2  16416  2lgs  16428  2lgsoddprmlem3  16435  uhgr0vb  16530  umgredg  16591  uspgrushgr  16626  uspgrupgr  16627  usgruspgr  16629  uhgr2edg  16652  edg0usgr  16693  egrsubgr  16709  0uhgrsubgr  16711  uhgrspansubgrlem  16722  vtxdg0v  16740  wlkpropg  16770  wlkv  16772  wlkvg  16774  wlkvtxeledgg  16790  wlkl1loop  16804  upgrwlkedg  16807  upgrwlkvtxedg  16810  uspgr2wlkeq  16811  wlkv0  16815  clwwlkccat  16847  clwwlknp  16863  clwwlkext2edg  16868  eupth2lem3lem4fi  16919  bj-elssuniab  17024  bj-nn0sucALT  17209  triap  17284