Theorem sylbird 169

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 157	. 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 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  drex1  1791  eqreu  2922  onsucsssucr  4493  ordsucunielexmid  4515  ovi3  5989  tfrlem9  6298  dom2lem  6750  distrlem4prl  7546  distrlem4pru  7547  recexprlemm  7586  caucvgprlem1  7641  caucvgprprlemexb  7669  aptisr  7741  map2psrprg  7767  renegcl  8180  addid0  8292  remulext2  8519  mulext1  8531  apmul1  8705  nnge1  8901  0mnnnnn0  9167  nn0lt2  9293  zneo  9313  uzind2  9324  fzind  9327  nn0ind-raph  9329  ledivge1le  9683  elfzmlbp  10088  difelfznle  10091  elfzodifsumelfzo  10157  ssfzo12  10180  flqeqceilz  10274  addmodlteq  10354  uzsinds  10398  qsqeqor  10586  facdiv  10672  facwordi  10674  bcpasc  10700  addcn2  11273  mulcn2  11275  climrecvg1n  11311  odd2np1  11832  oddge22np1  11840  gcdaddm  11939  algcvgblem  12003  cncongr1  12057  pcdvdsb  12273  pcaddlem  12292  infpnlem1  12311  prmunb  12314  metss2lem  13291  2sqlem6  13750