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  1798  eqreu  2930  onsucsssucr  4509  ordsucunielexmid  4531  ovi3  6011  tfrlem9  6320  dom2lem  6772  distrlem4prl  7583  distrlem4pru  7584  recexprlemm  7623  caucvgprlem1  7678  caucvgprprlemexb  7706  aptisr  7778  map2psrprg  7804  renegcl  8218  addid0  8330  remulext2  8557  mulext1  8569  apmul1  8745  nnge1  8942  0mnnnnn0  9208  nn0lt2  9334  zneo  9354  uzind2  9365  fzind  9368  nn0ind-raph  9370  ledivge1le  9726  elfzmlbp  10132  difelfznle  10135  elfzodifsumelfzo  10201  ssfzo12  10224  flqeqceilz  10318  addmodlteq  10398  uzsinds  10442  qsqeqor  10631  facdiv  10718  facwordi  10720  bcpasc  10746  addcn2  11318  mulcn2  11320  climrecvg1n  11356  odd2np1  11878  oddge22np1  11886  gcdaddm  11985  algcvgblem  12049  cncongr1  12103  pcdvdsb  12319  pcaddlem  12338  infpnlem1  12357  prmunb  12360  imasaddfnlemg  12735  subrgdvds  13356  aprcotr  13375  metss2lem  14000  lgseisenlem2  14454  2sqlem6  14470