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  1786  eqreu  2918  onsucsssucr  4486  ordsucunielexmid  4508  ovi3  5978  tfrlem9  6287  dom2lem  6738  distrlem4prl  7525  distrlem4pru  7526  recexprlemm  7565  caucvgprlem1  7620  caucvgprprlemexb  7648  aptisr  7720  map2psrprg  7746  renegcl  8159  addid0  8271  remulext2  8498  mulext1  8510  apmul1  8684  nnge1  8880  0mnnnnn0  9146  nn0lt2  9272  zneo  9292  uzind2  9303  fzind  9306  nn0ind-raph  9308  ledivge1le  9662  elfzmlbp  10067  difelfznle  10070  elfzodifsumelfzo  10136  ssfzo12  10159  flqeqceilz  10253  addmodlteq  10333  uzsinds  10377  qsqeqor  10565  facdiv  10651  facwordi  10653  bcpasc  10679  addcn2  11251  mulcn2  11253  climrecvg1n  11289  odd2np1  11810  oddge22np1  11818  gcdaddm  11917  algcvgblem  11981  cncongr1  12035  pcdvdsb  12251  pcaddlem  12270  infpnlem1  12289  prmunb  12292  metss2lem  13137  2sqlem6  13596