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  4506  ordsucunielexmid  4528  ovi3  6006  tfrlem9  6315  dom2lem  6767  distrlem4prl  7578  distrlem4pru  7579  recexprlemm  7618  caucvgprlem1  7673  caucvgprprlemexb  7701  aptisr  7773  map2psrprg  7799  renegcl  8212  addid0  8324  remulext2  8551  mulext1  8563  apmul1  8739  nnge1  8936  0mnnnnn0  9202  nn0lt2  9328  zneo  9348  uzind2  9359  fzind  9362  nn0ind-raph  9364  ledivge1le  9720  elfzmlbp  10125  difelfznle  10128  elfzodifsumelfzo  10194  ssfzo12  10217  flqeqceilz  10311  addmodlteq  10391  uzsinds  10435  qsqeqor  10623  facdiv  10709  facwordi  10711  bcpasc  10737  addcn2  11309  mulcn2  11311  climrecvg1n  11347  odd2np1  11868  oddge22np1  11876  gcdaddm  11975  algcvgblem  12039  cncongr1  12093  pcdvdsb  12309  pcaddlem  12328  infpnlem1  12347  prmunb  12350  aprcotr  13242  metss2lem  13779  2sqlem6  14238