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  3028  opeldmg  4882  elreldm  4903  ssimaex  5639  resflem  5743  f1eqcocnv  5859  fliftfun  5864  isopolem  5890  isosolem  5892  brtposg  6339  issmo2  6374  nnmcl  6566  nnawordi  6600  nnmordi  6601  nnmord  6602  swoord1  6648  ecopovtrn  6718  ecopovtrng  6721  f1domg  6848  mapen  6942  mapxpen  6944  supmoti  7094  isotilem  7107  exmidomniim  7242  enq0tr  7546  prubl  7598  ltexprlemloc  7719  addextpr  7733  recexprlem1ssl  7745  recexprlem1ssu  7746  cauappcvgprlemdisj  7763  mulcmpblnr  7853  mulgt0sr  7890  map2psrprg  7917  ltleletr  8153  ltle  8159  ltadd2  8491  leltadd  8519  reapti  8651  apreap  8659  reapcotr  8670  apcotr  8679  addext  8682  mulext1  8684  zapne  9446  zextle  9463  prime  9471  uzin  9680  indstr  9713  supinfneg  9715  infsupneg  9716  ublbneg  9733  xrltle  9919  xrre2  9942  icc0r  10047  fzrevral  10226  flqge  10423  modqadd1  10504  modqmul1  10520  facdiv  10881  elfzelfzccat  11054  resqrexlemgt0  11273  abs00ap  11315  absext  11316  climshftlemg  11555  climcaucn  11604  dvds2lem  12056  dvdsfac  12113  ltoddhalfle  12146  ndvdsadd  12184  bitsinv1lem  12214  gcdaddm  12247  bezoutlembi  12268  gcdzeq  12285  algcvga  12315  rpdvds  12363  cncongr1  12367  cncongr2  12368  prmind2  12384  euclemma  12410  isprm6  12411  rpexp  12417  sqrt2irr  12426  odzdvds  12510  pclemub  12552  pceulem  12559  pc2dvds  12595  fldivp1  12613  infpnlem1  12624  prmunb  12627  issubg4m  13471  imasabl  13614  fiinbas  14463  bastg  14475  tgcl  14478  opnssneib  14570  tgcnp  14623  iscnp4  14632  cnntr  14639  cnptopresti  14652  lmss  14660  lmtopcnp  14664  txdis  14691  xblss2ps  14818  xblss2  14819  blsscls2  14907  metequiv2  14910  bdxmet  14915  mulc1cncf  15003  cncfco  15005  sincosq2sgn  15241  sincosq3sgn  15242  sincosq4sgn  15243  lgsdir  15454  lgsquadlem2  15497  2sqlem8a  15541  2sqlem10  15544  triap  15901