Theorem sylbird 170

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbird.1	|- ( ph -> ( ch <-> ps ) )
sylbird.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
sylbird	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 |- ( ph -> ( ch <-> ps ) )
2	1	biimprd 158	. 2 |- ( ph -> ( ps -> ch ) )
3		sylbird.2	. 2 |- ( ph -> ( ch -> th ) )
4	2, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

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  1846  eqreu  2998  onsucsssucr  4607  ordsucunielexmid  4629  riotaeqimp  5995  ovi3  6158  tfrlem9  6484  dom2lem  6944  distrlem4prl  7803  distrlem4pru  7804  recexprlemm  7843  caucvgprlem1  7898  caucvgprprlemexb  7926  aptisr  7998  map2psrprg  8024  renegcl  8439  addid0  8551  remulext2  8779  mulext1  8791  apmul1  8967  nnge1  9165  0mnnnnn0  9433  nn0lt2  9560  zneo  9580  uzind2  9591  fzind  9594  nn0ind-raph  9596  ledivge1le  9960  elfzmlbp  10366  difelfznle  10369  elfzodifsumelfzo  10445  ssfzo12  10468  flqeqceilz  10579  addmodlteq  10659  uzsinds  10705  qsqeqor  10911  facdiv  10999  facwordi  11001  bcpasc  11027  ccatsymb  11178  swrdsbslen  11246  swrdspsleq  11247  swrdlsw  11249  swrdswrdlem  11284  swrdccatin1  11305  pfxccatin12lem3  11312  swrdccat  11315  pfxccat3a  11318  addcn2  11870  mulcn2  11872  climrecvg1n  11908  odd2np1  12433  oddge22np1  12441  bitsfzo  12515  gcdaddm  12554  algcvgblem  12620  cncongr1  12674  pcdvdsb  12892  pcaddlem  12911  infpnlem1  12931  prmunb  12934  imasaddfnlemg  13396  f1ghm0to0  13858  ghmf1  13859  imasring  14076  subrgdvds  14248  aprcotr  14298  quscrng  14546  metss2lem  15220  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  lgseisenlem2  15799  2sqlem6  15848  incistruhgr  15940  wlk1walkdom  16209  wlkv0  16219  clwwlkccatlem  16250