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  1617  ax11i  1701  equveli  1746  eupickbi  2095  nfabdw  2325  rgen2a  2518  reu6  2910  sseq0  3445  disjel  3458  preq12b  3744  prel12  3745  prneimg  3748  elinti  3827  exmidundif  4179  opthreg  4527  elreldm  4824  issref  4980  relcnvtr  5117  relresfld  5127  funopg  5216  funimass2  5260  f0dom0  5375  fvimacnv  5594  elunirn  5728  oprabid  5865  op1steq  6139  f1o2ndf1  6187  reldmtpos  6212  rntpos  6216  nntri3or  6452  nnaordex  6486  nnawordex  6487  findcard2  6846  findcard2s  6847  mkvprop  7113  cc2lem  7198  lt2addnq  7336  lt2mulnq  7337  genpelvl  7444  genpelvu  7445  distrlem5prl  7518  distrlem5pru  7519  caucvgprlemnkj  7598  map2psrprg  7737  rereceu  7821  ltxrlt  7955  0mnnnnn0  9137  elnnnn0b  9149  nn0le2is012  9264  btwnz  9301  uz11  9479  nn01to3  9546  zq  9555  xrltso  9723  xltnegi  9762  xnn0lenn0nn0  9792  xnn0xadd0  9794  iccleub  9858  fzdcel  9965  uznfz  10028  2ffzeq  10066  elfzonlteqm1  10135  icogelb  10191  flqeqceilz  10243  modqadd1  10286  modqmul1  10302  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  fzfig  10355  m1expeven  10492  caucvgrelemcau  10908  rexico  11149  fisumss  11319  fsum2dlemstep  11361  ntrivcvgap  11475  fprodssdc  11517  fprod2dlemstep  11549  0dvds  11737  alzdvds  11777  opoe  11817  omoe  11818  opeo  11819  omeo  11820  m1exp1  11823  nn0enne  11824  nn0o1gt2  11827  gcdneg  11900  dfgcd2  11932  algcvgblem  11960  algcvga  11962  eucalglt  11968  coprmdvds  12003  divgcdcoprmex  12013  cncongr1  12014  prm2orodd  12037  prm23lt5  12172  tg2  12601  tgcl  12605  neii1  12688  neii2  12690  txlm  12820  reopnap  13079  tgioo  13087  addcncntoplem  13092  bj-elssuniab  13507  bj-nn0sucALT  13695  triap  13742