Theorem sylbird 169

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 157	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	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  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  drex1  1786  eqreu  2917  onsucsssucr  4485  ordsucunielexmid  4507  ovi3  5974  tfrlem9  6283  dom2lem  6734  distrlem4prl  7521  distrlem4pru  7522  recexprlemm  7561  caucvgprlem1  7616  caucvgprprlemexb  7644  aptisr  7716  map2psrprg  7742  renegcl  8155  addid0  8267  remulext2  8494  mulext1  8506  apmul1  8680  nnge1  8876  0mnnnnn0  9142  nn0lt2  9268  zneo  9288  uzind2  9299  fzind  9302  nn0ind-raph  9304  ledivge1le  9658  elfzmlbp  10063  difelfznle  10066  elfzodifsumelfzo  10132  ssfzo12  10155  flqeqceilz  10249  addmodlteq  10329  uzsinds  10373  qsqeqor  10561  facdiv  10647  facwordi  10649  bcpasc  10675  addcn2  11247  mulcn2  11249  climrecvg1n  11285  odd2np1  11806  oddge22np1  11814  gcdaddm  11913  algcvgblem  11977  cncongr1  12031  pcdvdsb  12247  pcaddlem  12266  infpnlem1  12285  prmunb  12288  metss2lem  13097  2sqlem6  13556