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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.33bdc  1590  ax11i  1673  equveli  1713  eupickbi  2055  rgen2a  2458  reu6  2840  sseq0  3368  disjel  3381  preq12b  3661  prel12  3662  prneimg  3665  elinti  3744  exmidundif  4087  opthreg  4429  elreldm  4723  issref  4877  relcnvtr  5014  relresfld  5024  funopg  5113  funimass2  5157  f0dom0  5272  fvimacnv  5487  elunirn  5619  oprabid  5755  op1steq  6029  f1o2ndf1  6077  reldmtpos  6102  rntpos  6106  nntri3or  6341  nnaordex  6375  nnawordex  6376  findcard2  6734  findcard2s  6735  mkvprop  6979  lt2addnq  7154  lt2mulnq  7155  genpelvl  7262  genpelvu  7263  distrlem5prl  7336  distrlem5pru  7337  caucvgprlemnkj  7416  rereceu  7618  ltxrlt  7748  0mnnnnn0  8907  elnnnn0b  8919  nn0le2is012  9031  btwnz  9068  uz11  9244  nn01to3  9305  zq  9314  xrltso  9469  xltnegi  9505  xnn0lenn0nn0  9535  xnn0xadd0  9537  iccleub  9601  fzdcel  9707  uznfz  9770  2ffzeq  9805  elfzonlteqm1  9874  flqeqceilz  9978  modqadd1  10021  modqmul1  10037  frecuzrdgtcl  10072  frecuzrdgfunlem  10079  fzfig  10090  m1expeven  10227  caucvgrelemcau  10638  rexico  10879  fisumss  11047  fsum2dlemstep  11089  0dvds  11355  alzdvds  11394  opoe  11434  omoe  11435  opeo  11436  omeo  11437  m1exp1  11440  nn0enne  11441  nn0o1gt2  11444  gcdneg  11512  dfgcd2  11542  algcvgblem  11570  algcvga  11572  eucalglt  11578  coprmdvds  11613  divgcdcoprmex  11623  cncongr1  11624  prm2orodd  11647  tg2  12066  tgcl  12070  neii1  12153  neii2  12155  txlm  12284  tgioo  12526  addcncntoplem  12531  bj-elssuniab  12681  bj-nn0sucALT  12859  triap  12905