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  1812  eqreu  2956  onsucsssucr  4546  ordsucunielexmid  4568  ovi3  6064  tfrlem9  6386  dom2lem  6840  distrlem4prl  7670  distrlem4pru  7671  recexprlemm  7710  caucvgprlem1  7765  caucvgprprlemexb  7793  aptisr  7865  map2psrprg  7891  renegcl  8306  addid0  8418  remulext2  8646  mulext1  8658  apmul1  8834  nnge1  9032  0mnnnnn0  9300  nn0lt2  9426  zneo  9446  uzind2  9457  fzind  9460  nn0ind-raph  9462  ledivge1le  9820  elfzmlbp  10226  difelfznle  10229  elfzodifsumelfzo  10296  ssfzo12  10319  flqeqceilz  10429  addmodlteq  10509  uzsinds  10555  qsqeqor  10761  facdiv  10849  facwordi  10851  bcpasc  10877  addcn2  11494  mulcn2  11496  climrecvg1n  11532  odd2np1  12057  oddge22np1  12065  bitsfzo  12139  gcdaddm  12178  algcvgblem  12244  cncongr1  12298  pcdvdsb  12516  pcaddlem  12535  infpnlem1  12555  prmunb  12558  imasaddfnlemg  13018  f1ghm0to0  13480  ghmf1  13481  imasring  13698  subrgdvds  13869  aprcotr  13919  quscrng  14167  metss2lem  14819  gausslemma2dlem0i  15384  gausslemma2dlem1a  15385  lgseisenlem2  15398  2sqlem6  15447