Theorem syl6bi 162

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 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.33bdc  1609  ax11i  1692  equveli  1732  eupickbi  2081  rgen2a  2486  reu6  2873  sseq0  3404  disjel  3417  preq12b  3697  prel12  3698  prneimg  3701  elinti  3780  exmidundif  4129  opthreg  4471  elreldm  4765  issref  4921  relcnvtr  5058  relresfld  5068  funopg  5157  funimass2  5201  f0dom0  5316  fvimacnv  5535  elunirn  5667  oprabid  5803  op1steq  6077  f1o2ndf1  6125  reldmtpos  6150  rntpos  6154  nntri3or  6389  nnaordex  6423  nnawordex  6424  findcard2  6783  findcard2s  6784  mkvprop  7032  lt2addnq  7212  lt2mulnq  7213  genpelvl  7320  genpelvu  7321  distrlem5prl  7394  distrlem5pru  7395  caucvgprlemnkj  7474  map2psrprg  7613  rereceu  7697  ltxrlt  7830  0mnnnnn0  9009  elnnnn0b  9021  nn0le2is012  9133  btwnz  9170  uz11  9348  nn01to3  9409  zq  9418  xrltso  9582  xltnegi  9618  xnn0lenn0nn0  9648  xnn0xadd0  9650  iccleub  9714  fzdcel  9820  uznfz  9883  2ffzeq  9918  elfzonlteqm1  9987  flqeqceilz  10091  modqadd1  10134  modqmul1  10150  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  fzfig  10203  m1expeven  10340  caucvgrelemcau  10752  rexico  10993  fisumss  11161  fsum2dlemstep  11203  ntrivcvgap  11317  0dvds  11513  alzdvds  11552  opoe  11592  omoe  11593  opeo  11594  omeo  11595  m1exp1  11598  nn0enne  11599  nn0o1gt2  11602  gcdneg  11670  dfgcd2  11702  algcvgblem  11730  algcvga  11732  eucalglt  11738  coprmdvds  11773  divgcdcoprmex  11783  cncongr1  11784  prm2orodd  11807  tg2  12229  tgcl  12233  neii1  12316  neii2  12318  txlm  12448  reopnap  12707  tgioo  12715  addcncntoplem  12720  bj-elssuniab  12998  bj-nn0sucALT  13176  triap  13224