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  1679  ax11i  1762  equveli  1808  eupickbi  2163  nfabdw  2403  rgen2a  2596  reu6  3005  sseq0  3549  disjel  3562  preq12b  3873  prel12  3874  prneimg  3877  elinti  3957  exmidundif  4318  opthreg  4677  elreldm  4982  issref  5144  relcnvtr  5281  relresfld  5291  funopg  5385  funimass2  5433  f0dom0  5560  fvimacnv  5792  funopdmsn  5863  elunirn  5938  oprabid  6081  op1steq  6372  f1o2ndf1  6423  fvn0elsuppb  6451  suppfnss  6456  reldmtpos  6483  rntpos  6487  nntri3or  6725  nnaordex  6760  nnawordex  6761  findcard2  7145  findcard2s  7146  mkvprop  7448  cc2lem  7579  lt2addnq  7718  lt2mulnq  7719  genpelvl  7826  genpelvu  7827  distrlem5prl  7900  distrlem5pru  7901  caucvgprlemnkj  7980  map2psrprg  8119  rereceu  8203  ltxrlt  8338  0mnnnnn0  9527  elnnnn0b  9539  nn0le2is012  9659  btwnz  9696  uz11  9876  nn01to3  9948  zq  9957  xrltso  10128  xltnegi  10167  xnn0lenn0nn0  10197  xnn0xadd0  10199  iccleub  10263  fzdcel  10373  uznfz  10436  2ffzeq  10474  elfzonlteqm1  10554  icogelb  10624  flqeqceilz  10679  modqadd1  10722  modqmul1  10738  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  fzfig  10791  seqf1og  10882  m1expeven  10947  qsqeqor  11011  fundm2domnop0  11216  ccatrcl1  11298  pfxsuff1eqwrdeq  11387  wrdind  11410  wrd2ind  11411  swrdccat3blem  11427  caucvgrelemcau  11661  rexico  11902  fisumss  12074  fsum2dlemstep  12116  ntrivcvgap  12230  fprodssdc  12272  fprod2dlemstep  12304  0dvds  12493  alzdvds  12536  opoe  12577  omoe  12578  opeo  12579  omeo  12580  m1exp1  12583  nn0enne  12584  nn0o1gt2  12587  gcdneg  12674  dfgcd2  12706  algcvgblem  12742  algcvga  12744  eucalglt  12750  coprmdvds  12785  divgcdcoprmex  12795  cncongr1  12796  prm2orodd  12819  prm23lt5  12957  pockthi  13052  f1ocpbl  13516  f1ovscpbl  13517  f1olecpbl  13518  ismnddef  13623  lmodfopnelem1  14464  tg2  14917  tgcl  14921  neii1  15004  neii2  15006  txlm  15136  reopnap  15403  tgioo  15411  addcncntoplem  15418  gausslemma2dlem0i  15922  2lgslem2  15957  2lgs  15969  2lgsoddprmlem3  15976  uhgr0vb  16071  umgredg  16132  uspgrushgr  16167  uspgrupgr  16168  usgruspgr  16170  uhgr2edg  16193  edg0usgr  16234  egrsubgr  16250  0uhgrsubgr  16252  uhgrspansubgrlem  16263  vtxdg0v  16281  wlkpropg  16311  wlkv  16313  wlkvg  16315  wlkvtxeledgg  16331  wlkl1loop  16345  upgrwlkedg  16348  upgrwlkvtxedg  16351  uspgr2wlkeq  16352  wlkv0  16356  clwwlkccat  16388  clwwlknp  16404  clwwlkext2edg  16409  eupth2lem3lem4fi  16460  bj-elssuniab  16555  bj-nn0sucALT  16740  triap  16805