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  2994  opeldmg  4833  elreldm  4854  ssimaex  5578  resflem  5681  f1eqcocnv  5792  fliftfun  5797  isopolem  5823  isosolem  5825  brtposg  6255  issmo2  6290  nnmcl  6482  nnawordi  6516  nnmordi  6517  nnmord  6518  swoord1  6564  ecopovtrn  6632  ecopovtrng  6635  f1domg  6758  mapen  6846  mapxpen  6848  supmoti  6992  isotilem  7005  exmidomniim  7139  enq0tr  7433  prubl  7485  ltexprlemloc  7606  addextpr  7620  recexprlem1ssl  7632  recexprlem1ssu  7633  cauappcvgprlemdisj  7650  mulcmpblnr  7740  mulgt0sr  7777  map2psrprg  7804  ltleletr  8039  ltle  8045  ltadd2  8376  leltadd  8404  reapti  8536  apreap  8544  reapcotr  8555  apcotr  8564  addext  8567  mulext1  8569  zapne  9327  zextle  9344  prime  9352  uzin  9560  indstr  9593  supinfneg  9595  infsupneg  9596  ublbneg  9613  xrltle  9798  xrre2  9821  icc0r  9926  fzrevral  10105  flqge  10282  modqadd1  10361  modqmul1  10377  facdiv  10718  resqrexlemgt0  11029  abs00ap  11071  absext  11072  climshftlemg  11310  climcaucn  11359  dvds2lem  11810  dvdsfac  11866  ltoddhalfle  11898  ndvdsadd  11936  gcdaddm  11985  bezoutlembi  12006  gcdzeq  12023  algcvga  12051  rpdvds  12099  cncongr1  12103  cncongr2  12104  prmind2  12120  euclemma  12146  isprm6  12147  rpexp  12153  sqrt2irr  12162  odzdvds  12245  pclemub  12287  pceulem  12294  pc2dvds  12329  fldivp1  12346  infpnlem1  12357  prmunb  12360  issubg4m  13053  fiinbas  13552  bastg  13564  tgcl  13567  opnssneib  13659  tgcnp  13712  iscnp4  13721  cnntr  13728  cnptopresti  13741  lmss  13749  lmtopcnp  13753  txdis  13780  xblss2ps  13907  xblss2  13908  blsscls2  13996  metequiv2  13999  bdxmet  14004  mulc1cncf  14079  cncfco  14081  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  lgsdir  14439  2sqlem8a  14472  2sqlem10  14475  triap  14780