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  3008  onsucsssucr  4630  ordsucunielexmid  4652  riotaeqimp  6027  ovi3  6190  suppssrst  6460  suppssrgst  6461  tfrlem9  6549  dom2lem  7010  distrlem4prl  7895  distrlem4pru  7896  recexprlemm  7935  caucvgprlem1  7990  caucvgprprlemexb  8018  aptisr  8090  map2psrprg  8116  renegcl  8530  addid0  8642  remulext2  8870  mulext1  8882  apmul1  9058  nnge1  9256  0mnnnnn0  9524  nn0lt2  9655  zneo  9675  uzind2  9686  fzind  9689  nn0ind-raph  9691  ledivge1le  10055  elfzmlbp  10462  difelfznle  10465  elfzodifsumelfzo  10542  ssfzo12  10565  flqeqceilz  10676  addmodlteq  10756  uzsinds  10802  qsqeqor  11008  facdiv  11096  facwordi  11098  bcpasc  11124  ccatsymb  11283  swrdsbslen  11351  swrdspsleq  11352  swrdlsw  11354  swrdswrdlem  11389  swrdccatin1  11410  pfxccatin12lem3  11417  swrdccat  11420  pfxccat3a  11423  addcn2  11988  mulcn2  11990  climrecvg1n  12026  odd2np1  12552  oddge22np1  12560  bitsfzo  12634  gcdaddm  12673  algcvgblem  12739  cncongr1  12793  pcdvdsb  13011  pcaddlem  13030  infpnlem1  13050  prmunb  13053  imasaddfnlemg  13516  f1ghm0to0  13978  ghmf1  13979  imasring  14197  subrgdvds  14369  aprcotr  14420  quscrng  14668  metss2lem  15349  pellexlem1  15832  gausslemma2dlem0i  15917  gausslemma2dlem1a  15918  lgseisenlem2  15931  2sqlem6  15980  incistruhgr  16072  wlk1walkdom  16341  wlkv0  16351  clwwlkccatlem  16382