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  1824  eqreu  2975  onsucsssucr  4578  ordsucunielexmid  4600  riotaeqimp  5952  ovi3  6113  tfrlem9  6435  dom2lem  6893  distrlem4prl  7739  distrlem4pru  7740  recexprlemm  7779  caucvgprlem1  7834  caucvgprprlemexb  7862  aptisr  7934  map2psrprg  7960  renegcl  8375  addid0  8487  remulext2  8715  mulext1  8727  apmul1  8903  nnge1  9101  0mnnnnn0  9369  nn0lt2  9496  zneo  9516  uzind2  9527  fzind  9530  nn0ind-raph  9532  ledivge1le  9890  elfzmlbp  10296  difelfznle  10299  elfzodifsumelfzo  10374  ssfzo12  10397  flqeqceilz  10507  addmodlteq  10587  uzsinds  10633  qsqeqor  10839  facdiv  10927  facwordi  10929  bcpasc  10955  ccatsymb  11103  swrdsbslen  11164  swrdspsleq  11165  swrdlsw  11167  swrdswrdlem  11202  swrdccatin1  11223  pfxccatin12lem3  11230  swrdccat  11233  pfxccat3a  11236  addcn2  11787  mulcn2  11789  climrecvg1n  11825  odd2np1  12350  oddge22np1  12358  bitsfzo  12432  gcdaddm  12471  algcvgblem  12537  cncongr1  12591  pcdvdsb  12809  pcaddlem  12828  infpnlem1  12848  prmunb  12851  imasaddfnlemg  13313  f1ghm0to0  13775  ghmf1  13776  imasring  13993  subrgdvds  14164  aprcotr  14214  quscrng  14462  metss2lem  15136  gausslemma2dlem0i  15701  gausslemma2dlem1a  15702  lgseisenlem2  15715  2sqlem6  15764  incistruhgr  15855