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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3d  202  drex1  1851  eqreu  3018  onsucsssucr  4658  ordsucunielexmid  4680  riotaeqimp  6066  ovi3  6229  suppssrst  6505  suppssrgst  6506  tfrlem9  6594  dom2lem  7063  distrlem4prl  7958  distrlem4pru  7959  recexprlemm  7998  caucvgprlem1  8053  caucvgprprlemexb  8081  aptisr  8153  map2psrprg  8179  renegcl  8595  addid0  8707  remulext2  8937  mulext1  8949  apmul1  9127  nnge1  9337  0mnnnnn0  9607  nn0lt2  9739  zneo  9759  uzind2  9770  fzind  9773  nn0ind-raph  9775  ledivge1le  10145  elfzmlbp  10557  difelfznle  10560  elfzodifsumelfzo  10637  ssfzo12  10660  flqeqceilz  10777  addmodlteq  10857  uzsinds  10903  qsqeqor  11109  facdiv  11199  facwordi  11201  bcpasc  11227  ccatsymb  11393  swrdsbslen  11461  swrdspsleq  11462  swrdlsw  11464  swrdswrdlem  11499  swrdccatin1  11520  pfxccatin12lem3  11527  swrdccat  11530  pfxccat3a  11533  addcn2  12102  mulcn2  12104  climrecvg1n  12140  odd2np1  12666  oddge22np1  12674  bitsfzo  12748  gcdaddm  12787  algcvgblem  12853  cncongr1  12907  pcdvdsb  13129  pcaddlem  13148  infpnlem1  13168  prmunb  13171  imasaddfnlemg  13695  f1ghm0to0  14135  ghmf1  14136  gsumcom2fi  14276  imasring  14479  subrgdvds  14653  aprcotr  14707  quscrng  14980  rnasclassa  15148  metss2lem  15735  pellexlem1  16241  ppiqeq0  16292  chtqub  16308  bposlem6  16328  gausslemma2dlem0i  16393  gausslemma2dlem1a  16394  lgseisenlem2  16407  2sqlem6  16456  incistruhgr  16548  wlk1walkdom  16817  wlkv0  16827  clwwlkccatlem  16858