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  1676  ax11i  1760  equveli  1805  eupickbi  2160  nfabdw  2391  rgen2a  2584  reu6  2992  sseq0  3533  disjel  3546  preq12b  3848  prel12  3849  prneimg  3852  elinti  3932  exmidundif  4290  opthreg  4648  elreldm  4950  issref  5111  relcnvtr  5248  relresfld  5258  funopg  5352  funimass2  5399  f0dom0  5521  fvimacnv  5752  funopdmsn  5823  elunirn  5896  oprabid  6039  op1steq  6331  f1o2ndf1  6380  reldmtpos  6405  rntpos  6409  nntri3or  6647  nnaordex  6682  nnawordex  6683  findcard2  7059  findcard2s  7060  mkvprop  7336  cc2lem  7463  lt2addnq  7602  lt2mulnq  7603  genpelvl  7710  genpelvu  7711  distrlem5prl  7784  distrlem5pru  7785  caucvgprlemnkj  7864  map2psrprg  8003  rereceu  8087  ltxrlt  8223  0mnnnnn0  9412  elnnnn0b  9424  nn0le2is012  9540  btwnz  9577  uz11  9757  nn01to3  9824  zq  9833  xrltso  10004  xltnegi  10043  xnn0lenn0nn0  10073  xnn0xadd0  10075  iccleub  10139  fzdcel  10248  uznfz  10311  2ffzeq  10349  elfzonlteqm1  10428  icogelb  10497  flqeqceilz  10552  modqadd1  10595  modqmul1  10611  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  fzfig  10664  seqf1og  10755  m1expeven  10820  qsqeqor  10884  fundm2domnop0  11080  ccatrcl1  11162  pfxsuff1eqwrdeq  11246  wrdind  11269  wrd2ind  11270  swrdccat3blem  11286  caucvgrelemcau  11506  rexico  11747  fisumss  11918  fsum2dlemstep  11960  ntrivcvgap  12074  fprodssdc  12116  fprod2dlemstep  12148  0dvds  12337  alzdvds  12380  opoe  12421  omoe  12422  opeo  12423  omeo  12424  m1exp1  12427  nn0enne  12428  nn0o1gt2  12431  gcdneg  12518  dfgcd2  12550  algcvgblem  12586  algcvga  12588  eucalglt  12594  coprmdvds  12629  divgcdcoprmex  12639  cncongr1  12640  prm2orodd  12663  prm23lt5  12801  pockthi  12896  f1ocpbl  13359  f1ovscpbl  13360  f1olecpbl  13361  ismnddef  13466  lmodfopnelem1  14303  tg2  14749  tgcl  14753  neii1  14836  neii2  14838  txlm  14968  reopnap  15235  tgioo  15243  addcncntoplem  15250  gausslemma2dlem0i  15751  2lgslem2  15786  2lgs  15798  2lgsoddprmlem3  15805  uhgr0vb  15899  umgredg  15958  uspgrushgr  15993  uspgrupgr  15994  usgruspgr  15996  uhgr2edg  16019  vtxdg0v  16053  wlkpropg  16065  wlkv  16067  wlkvg  16069  wlkvtxeledgg  16085  wlkl1loop  16099  upgrwlkedg  16102  upgrwlkvtxedg  16105  uspgr2wlkeq  16106  wlkv0  16110  clwwlkccat  16138  bj-elssuniab  16210  bj-nn0sucALT  16396  triap  16457