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  1845  eqreu  2997  onsucsssucr  4609  ordsucunielexmid  4631  riotaeqimp  6001  ovi3  6164  tfrlem9  6490  dom2lem  6950  distrlem4prl  7809  distrlem4pru  7810  recexprlemm  7849  caucvgprlem1  7904  caucvgprprlemexb  7932  aptisr  8004  map2psrprg  8030  renegcl  8445  addid0  8557  remulext2  8785  mulext1  8797  apmul1  8973  nnge1  9171  0mnnnnn0  9439  nn0lt2  9566  zneo  9586  uzind2  9597  fzind  9600  nn0ind-raph  9602  ledivge1le  9966  elfzmlbp  10372  difelfznle  10375  elfzodifsumelfzo  10452  ssfzo12  10475  flqeqceilz  10586  addmodlteq  10666  uzsinds  10712  qsqeqor  10918  facdiv  11006  facwordi  11008  bcpasc  11034  ccatsymb  11188  swrdsbslen  11256  swrdspsleq  11257  swrdlsw  11259  swrdswrdlem  11294  swrdccatin1  11315  pfxccatin12lem3  11322  swrdccat  11325  pfxccat3a  11328  addcn2  11893  mulcn2  11895  climrecvg1n  11931  odd2np1  12457  oddge22np1  12465  bitsfzo  12539  gcdaddm  12578  algcvgblem  12644  cncongr1  12698  pcdvdsb  12916  pcaddlem  12935  infpnlem1  12955  prmunb  12958  imasaddfnlemg  13420  f1ghm0to0  13882  ghmf1  13883  imasring  14101  subrgdvds  14273  aprcotr  14323  quscrng  14571  metss2lem  15250  gausslemma2dlem0i  15815  gausslemma2dlem1a  15816  lgseisenlem2  15829  2sqlem6  15878  incistruhgr  15970  wlk1walkdom  16239  wlkv0  16249  clwwlkccatlem  16280