Theorem syl6bi 161

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
syl6bi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
syl6bi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6bi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 142	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.33bdc  1562  ax11i  1644  equveli  1684  eupickbi  2025  rgen2a  2423  reu6  2792  sseq0  3306  disjel  3319  preq12b  3588  prel12  3589  prneimg  3592  elinti  3671  exmidundif  3999  opthreg  4335  elreldm  4619  issref  4769  relcnvtr  4904  relresfld  4914  funopg  5001  funimass2  5045  f0dom0  5152  fvimacnv  5359  elunirn  5485  oprabid  5616  op1steq  5884  f1o2ndf1  5928  reldmtpos  5950  rntpos  5954  nntri3or  6186  nnaordex  6216  nnawordex  6217  findcard2  6535  findcard2s  6536  lt2addnq  6866  lt2mulnq  6867  genpelvl  6974  genpelvu  6975  distrlem5prl  7048  distrlem5pru  7049  caucvgprlemnkj  7128  rereceu  7327  ltxrlt  7455  0mnnnnn0  8597  elnnnn0b  8609  btwnz  8761  uz11  8936  nn01to3  8997  zq  9006  xrltso  9161  xltnegi  9192  iccleub  9244  fzdcel  9349  uznfz  9410  2ffzeq  9442  elfzonlteqm1  9510  flqeqceilz  9614  modqadd1  9657  modqmul1  9673  frecuzrdgtcl  9708  frecuzrdgfunlem  9715  fzfig  9726  m1expeven  9839  caucvgrelemcau  10240  rexico  10481  0dvds  10596  alzdvds  10635  opoe  10675  omoe  10676  opeo  10677  omeo  10678  m1exp1  10681  nn0enne  10682  nn0o1gt2  10685  gcdneg  10753  dfgcd2  10783  algcvgblem  10811  ialgcvga  10813  eucalglt  10819  coprmdvds  10854  divgcdcoprmex  10864  cncongr1  10865  prm2orodd  10888  bj-elssuniab  11034  bj-nn0sucALT  11216