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  1809  eqreu  2952  onsucsssucr  4541  ordsucunielexmid  4563  ovi3  6055  tfrlem9  6372  dom2lem  6826  distrlem4prl  7644  distrlem4pru  7645  recexprlemm  7684  caucvgprlem1  7739  caucvgprprlemexb  7767  aptisr  7839  map2psrprg  7865  renegcl  8280  addid0  8392  remulext2  8619  mulext1  8631  apmul1  8807  nnge1  9005  0mnnnnn0  9272  nn0lt2  9398  zneo  9418  uzind2  9429  fzind  9432  nn0ind-raph  9434  ledivge1le  9792  elfzmlbp  10198  difelfznle  10201  elfzodifsumelfzo  10268  ssfzo12  10291  flqeqceilz  10389  addmodlteq  10469  uzsinds  10515  qsqeqor  10721  facdiv  10809  facwordi  10811  bcpasc  10837  addcn2  11453  mulcn2  11455  climrecvg1n  11491  odd2np1  12014  oddge22np1  12022  gcdaddm  12121  algcvgblem  12187  cncongr1  12241  pcdvdsb  12458  pcaddlem  12477  infpnlem1  12497  prmunb  12500  imasaddfnlemg  12897  f1ghm0to0  13342  ghmf1  13343  imasring  13560  subrgdvds  13731  aprcotr  13781  quscrng  14029  metss2lem  14665  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  lgseisenlem2  15187  2sqlem6  15207