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  1847  eqreu  3012  onsucsssucr  4636  ordsucunielexmid  4658  riotaeqimp  6036  ovi3  6199  suppssrst  6474  suppssrgst  6475  tfrlem9  6563  dom2lem  7024  distrlem4prl  7915  distrlem4pru  7916  recexprlemm  7955  caucvgprlem1  8010  caucvgprprlemexb  8038  aptisr  8110  map2psrprg  8136  renegcl  8551  addid0  8663  remulext2  8892  mulext1  8904  apmul1  9082  nnge1  9280  0mnnnnn0  9548  nn0lt2  9680  zneo  9700  uzind2  9711  fzind  9714  nn0ind-raph  9716  ledivge1le  10080  elfzmlbp  10491  difelfznle  10494  elfzodifsumelfzo  10571  ssfzo12  10594  flqeqceilz  10707  addmodlteq  10787  uzsinds  10833  qsqeqor  11039  facdiv  11128  facwordi  11130  bcpasc  11156  ccatsymb  11318  swrdsbslen  11386  swrdspsleq  11387  swrdlsw  11389  swrdswrdlem  11424  swrdccatin1  11445  pfxccatin12lem3  11452  swrdccat  11455  pfxccat3a  11458  addcn2  12023  mulcn2  12025  climrecvg1n  12061  odd2np1  12587  oddge22np1  12595  bitsfzo  12669  gcdaddm  12708  algcvgblem  12774  cncongr1  12828  pcdvdsb  13046  pcaddlem  13065  infpnlem1  13085  prmunb  13088  imasaddfnlemg  13581  f1ghm0to0  14028  ghmf1  14029  imasring  14310  subrgdvds  14484  aprcotr  14538  quscrng  14810  metss2lem  15491  pellexlem1  15974  gausslemma2dlem0i  16059  gausslemma2dlem1a  16060  lgseisenlem2  16073  2sqlem6  16122  incistruhgr  16214  wlk1walkdom  16483  wlkv0  16493  clwwlkccatlem  16524