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  1846  eqreu  2998  onsucsssucr  4607  ordsucunielexmid  4629  riotaeqimp  5996  ovi3  6159  tfrlem9  6485  dom2lem  6945  distrlem4prl  7804  distrlem4pru  7805  recexprlemm  7844  caucvgprlem1  7899  caucvgprprlemexb  7927  aptisr  7999  map2psrprg  8025  renegcl  8440  addid0  8552  remulext2  8780  mulext1  8792  apmul1  8968  nnge1  9166  0mnnnnn0  9434  nn0lt2  9561  zneo  9581  uzind2  9592  fzind  9595  nn0ind-raph  9597  ledivge1le  9961  elfzmlbp  10367  difelfznle  10370  elfzodifsumelfzo  10447  ssfzo12  10470  flqeqceilz  10581  addmodlteq  10661  uzsinds  10707  qsqeqor  10913  facdiv  11001  facwordi  11003  bcpasc  11029  ccatsymb  11180  swrdsbslen  11248  swrdspsleq  11249  swrdlsw  11251  swrdswrdlem  11286  swrdccatin1  11307  pfxccatin12lem3  11314  swrdccat  11317  pfxccat3a  11320  addcn2  11872  mulcn2  11874  climrecvg1n  11910  odd2np1  12436  oddge22np1  12444  bitsfzo  12518  gcdaddm  12557  algcvgblem  12623  cncongr1  12677  pcdvdsb  12895  pcaddlem  12914  infpnlem1  12934  prmunb  12937  imasaddfnlemg  13399  f1ghm0to0  13861  ghmf1  13862  imasring  14080  subrgdvds  14252  aprcotr  14302  quscrng  14550  metss2lem  15224  gausslemma2dlem0i  15789  gausslemma2dlem1a  15790  lgseisenlem2  15803  2sqlem6  15852  incistruhgr  15944  wlk1walkdom  16213  wlkv0  16223  clwwlkccatlem  16254