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  3011  onsucsssucr  4633  ordsucunielexmid  4655  riotaeqimp  6030  ovi3  6193  suppssrst  6463  suppssrgst  6464  tfrlem9  6552  dom2lem  7013  distrlem4prl  7904  distrlem4pru  7905  recexprlemm  7944  caucvgprlem1  7999  caucvgprprlemexb  8027  aptisr  8099  map2psrprg  8125  renegcl  8539  addid0  8651  remulext2  8879  mulext1  8891  apmul1  9067  nnge1  9265  0mnnnnn0  9533  nn0lt2  9665  zneo  9685  uzind2  9696  fzind  9699  nn0ind-raph  9701  ledivge1le  10065  elfzmlbp  10473  difelfznle  10476  elfzodifsumelfzo  10553  ssfzo12  10576  flqeqceilz  10687  addmodlteq  10767  uzsinds  10813  qsqeqor  11019  facdiv  11108  facwordi  11110  bcpasc  11136  ccatsymb  11298  swrdsbslen  11366  swrdspsleq  11367  swrdlsw  11369  swrdswrdlem  11404  swrdccatin1  11425  pfxccatin12lem3  11432  swrdccat  11435  pfxccat3a  11438  addcn2  12003  mulcn2  12005  climrecvg1n  12041  odd2np1  12567  oddge22np1  12575  bitsfzo  12649  gcdaddm  12688  algcvgblem  12754  cncongr1  12808  pcdvdsb  13026  pcaddlem  13045  infpnlem1  13065  prmunb  13068  imasaddfnlemg  13548  f1ghm0to0  14010  ghmf1  14011  imasring  14229  subrgdvds  14403  aprcotr  14457  quscrng  14730  metss2lem  15411  pellexlem1  15894  gausslemma2dlem0i  15979  gausslemma2dlem1a  15980  lgseisenlem2  15993  2sqlem6  16042  incistruhgr  16134  wlk1walkdom  16403  wlkv0  16413  clwwlkccatlem  16444