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  1566  ax11i  1649  equveli  1689  eupickbi  2030  rgen2a  2429  reu6  2802  sseq0  3321  disjel  3334  preq12b  3609  prel12  3610  prneimg  3613  elinti  3692  exmidundif  4026  opthreg  4362  elreldm  4649  issref  4801  relcnvtr  4937  relresfld  4947  funopg  5034  funimass2  5078  f0dom0  5188  fvimacnv  5398  elunirn  5527  oprabid  5663  op1steq  5931  f1o2ndf1  5975  reldmtpos  6000  rntpos  6004  nntri3or  6236  nnaordex  6266  nnawordex  6267  findcard2  6585  findcard2s  6586  lt2addnq  6942  lt2mulnq  6943  genpelvl  7050  genpelvu  7051  distrlem5prl  7124  distrlem5pru  7125  caucvgprlemnkj  7204  rereceu  7403  ltxrlt  7531  0mnnnnn0  8675  elnnnn0b  8687  btwnz  8835  uz11  9010  nn01to3  9071  zq  9080  xrltso  9235  xltnegi  9266  iccleub  9318  fzdcel  9423  uznfz  9484  2ffzeq  9517  elfzonlteqm1  9586  flqeqceilz  9690  modqadd1  9733  modqmul1  9749  frecuzrdgtcl  9784  frecuzrdgfunlem  9791  fzfig  9802  m1expeven  9967  caucvgrelemcau  10378  rexico  10619  fisumss  10748  fsum2dlemstep  10791  0dvds  10898  alzdvds  10937  opoe  10977  omoe  10978  opeo  10979  omeo  10980  m1exp1  10983  nn0enne  10984  nn0o1gt2  10987  gcdneg  11055  dfgcd2  11085  algcvgblem  11113  ialgcvga  11115  eucalglt  11121  coprmdvds  11156  divgcdcoprmex  11166  cncongr1  11167  prm2orodd  11190  bj-elssuniab  11337  bj-nn0sucALT  11519