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  1618  ax11i  1702  equveli  1747  eupickbi  2096  nfabdw  2327  rgen2a  2520  reu6  2915  sseq0  3450  disjel  3463  preq12b  3750  prel12  3751  prneimg  3754  elinti  3833  exmidundif  4185  opthreg  4533  elreldm  4830  issref  4986  relcnvtr  5123  relresfld  5133  funopg  5222  funimass2  5266  f0dom0  5381  fvimacnv  5600  elunirn  5734  oprabid  5874  op1steq  6147  f1o2ndf1  6196  reldmtpos  6221  rntpos  6225  nntri3or  6461  nnaordex  6495  nnawordex  6496  findcard2  6855  findcard2s  6856  mkvprop  7122  cc2lem  7207  lt2addnq  7345  lt2mulnq  7346  genpelvl  7453  genpelvu  7454  distrlem5prl  7527  distrlem5pru  7528  caucvgprlemnkj  7607  map2psrprg  7746  rereceu  7830  ltxrlt  7964  0mnnnnn0  9146  elnnnn0b  9158  nn0le2is012  9273  btwnz  9310  uz11  9488  nn01to3  9555  zq  9564  xrltso  9732  xltnegi  9771  xnn0lenn0nn0  9801  xnn0xadd0  9803  iccleub  9867  fzdcel  9975  uznfz  10038  2ffzeq  10076  elfzonlteqm1  10145  icogelb  10201  flqeqceilz  10253  modqadd1  10296  modqmul1  10312  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  fzfig  10365  m1expeven  10502  qsqeqor  10565  caucvgrelemcau  10922  rexico  11163  fisumss  11333  fsum2dlemstep  11375  ntrivcvgap  11489  fprodssdc  11531  fprod2dlemstep  11563  0dvds  11751  alzdvds  11792  opoe  11832  omoe  11833  opeo  11834  omeo  11835  m1exp1  11838  nn0enne  11839  nn0o1gt2  11842  gcdneg  11915  dfgcd2  11947  algcvgblem  11981  algcvga  11983  eucalglt  11989  coprmdvds  12024  divgcdcoprmex  12034  cncongr1  12035  prm2orodd  12058  prm23lt5  12195  pockthi  12288  tg2  12700  tgcl  12704  neii1  12787  neii2  12789  txlm  12919  reopnap  13178  tgioo  13186  addcncntoplem  13191  bj-elssuniab  13672  bj-nn0sucALT  13860  triap  13908