Theorem sylbird 170

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbird.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
sylbird.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbird	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 158	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  drex1  1798  eqreu  2929  onsucsssucr  4508  ordsucunielexmid  4530  ovi3  6010  tfrlem9  6319  dom2lem  6771  distrlem4prl  7582  distrlem4pru  7583  recexprlemm  7622  caucvgprlem1  7677  caucvgprprlemexb  7705  aptisr  7777  map2psrprg  7803  renegcl  8217  addid0  8329  remulext2  8556  mulext1  8568  apmul1  8744  nnge1  8941  0mnnnnn0  9207  nn0lt2  9333  zneo  9353  uzind2  9364  fzind  9367  nn0ind-raph  9369  ledivge1le  9725  elfzmlbp  10131  difelfznle  10134  elfzodifsumelfzo  10200  ssfzo12  10223  flqeqceilz  10317  addmodlteq  10397  uzsinds  10441  qsqeqor  10630  facdiv  10717  facwordi  10719  bcpasc  10745  addcn2  11317  mulcn2  11319  climrecvg1n  11355  odd2np1  11877  oddge22np1  11885  gcdaddm  11984  algcvgblem  12048  cncongr1  12102  pcdvdsb  12318  pcaddlem  12337  infpnlem1  12356  prmunb  12359  imasaddfnlemg  12734  subrgdvds  13354  aprcotr  13373  metss2lem  13967  lgseisenlem2  14421  2sqlem6  14437