Theorem sylibrd 169

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

Hypotheses

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

Assertion

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

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylibrd.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	2	biimprd 158	. 2 |- ( ph -> ( ch -> th ) )
4	1, 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:  3imtr4d  203  sbciegft  3020  opeldmg  4872  elreldm  4893  ssimaex  5625  resflem  5729  f1eqcocnv  5841  fliftfun  5846  isopolem  5872  isosolem  5874  brtposg  6321  issmo2  6356  nnmcl  6548  nnawordi  6582  nnmordi  6583  nnmord  6584  swoord1  6630  ecopovtrn  6700  ecopovtrng  6703  f1domg  6826  mapen  6916  mapxpen  6918  supmoti  7068  isotilem  7081  exmidomniim  7216  enq0tr  7520  prubl  7572  ltexprlemloc  7693  addextpr  7707  recexprlem1ssl  7719  recexprlem1ssu  7720  cauappcvgprlemdisj  7737  mulcmpblnr  7827  mulgt0sr  7864  map2psrprg  7891  ltleletr  8127  ltle  8133  ltadd2  8465  leltadd  8493  reapti  8625  apreap  8633  reapcotr  8644  apcotr  8653  addext  8656  mulext1  8658  zapne  9419  zextle  9436  prime  9444  uzin  9653  indstr  9686  supinfneg  9688  infsupneg  9689  ublbneg  9706  xrltle  9892  xrre2  9915  icc0r  10020  fzrevral  10199  flqge  10391  modqadd1  10472  modqmul1  10488  facdiv  10849  resqrexlemgt0  11204  abs00ap  11246  absext  11247  climshftlemg  11486  climcaucn  11535  dvds2lem  11987  dvdsfac  12044  ltoddhalfle  12077  ndvdsadd  12115  bitsinv1lem  12145  gcdaddm  12178  bezoutlembi  12199  gcdzeq  12216  algcvga  12246  rpdvds  12294  cncongr1  12298  cncongr2  12299  prmind2  12315  euclemma  12341  isprm6  12342  rpexp  12348  sqrt2irr  12357  odzdvds  12441  pclemub  12483  pceulem  12490  pc2dvds  12526  fldivp1  12544  infpnlem1  12555  prmunb  12558  issubg4m  13401  imasabl  13544  fiinbas  14393  bastg  14405  tgcl  14408  opnssneib  14500  tgcnp  14553  iscnp4  14562  cnntr  14569  cnptopresti  14582  lmss  14590  lmtopcnp  14594  txdis  14621  xblss2ps  14748  xblss2  14749  blsscls2  14837  metequiv2  14840  bdxmet  14845  mulc1cncf  14933  cncfco  14935  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  lgsdir  15384  lgsquadlem2  15427  2sqlem8a  15471  2sqlem10  15474  triap  15786