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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  sbciegft  3082  opeldmg  4986  elreldm  5008  ssimaex  5764  resflem  5872  f1eqcocnv  5997  fliftfun  6002  isopolem  6028  isosolem  6030  brtposg  6525  issmo2  6560  nnmcl  6754  nnawordi  6788  nnmordi  6789  nnmord  6790  swoord1  6836  ecopovtrn  6906  ecopovtrng  6909  f1domg  7044  mapen  7146  mapxpen  7148  mapunen  7151  supmoti  7333  isotilem  7346  exmidomniim  7481  enq0tr  7801  prubl  7853  ltexprlemloc  7974  addextpr  7988  recexprlem1ssl  8000  recexprlem1ssu  8001  cauappcvgprlemdisj  8018  mulcmpblnr  8108  mulgt0sr  8145  map2psrprg  8172  ltleletr  8407  ltle  8413  ltadd2  8747  leltadd  8775  reapti  8907  apreap  8915  reapcotr  8926  apcotr  8935  addext  8938  mulext1  8940  zapne  9719  zextle  9737  prime  9745  uzin  9955  indstr  9993  supinfneg  9995  infsupneg  9996  ublbneg  10013  xrltle  10200  xrre2  10223  icc0r  10328  fzrevral  10512  flqge  10717  modqadd1  10798  modqmul1  10814  facdiv  11176  elfzelfzccat  11368  resqrexlemgt0  11786  abs00ap  11828  absext  11829  climshftlemg  12068  climcaucn  12117  dvds2lem  12570  dvdsfac  12627  ltoddhalfle  12660  ndvdsadd  12698  bitsinv1lem  12728  gcdaddm  12761  bezoutlembi  12782  gcdzeq  12799  algcvga  12829  rpdvds  12877  cncongr1  12881  cncongr2  12882  prmind2  12898  euclemma  12924  isprm6  12925  rpexp  12931  sqrt2irr  12940  odzdvds  13024  pclemub  13066  pceulem  13073  pc2dvds  13109  fldivp1  13127  infpnlem1  13138  prmunb  13141  ballotfilem7  13279  issubg4m  13996  imasabl  14140  fiinbas  15150  bastg  15162  tgcl  15165  opnssneib  15257  tgcnp  15310  iscnp4  15319  cnntr  15326  cnptopresti  15339  lmss  15347  lmtopcnp  15351  txdis  15378  xblss2ps  15505  xblss2  15506  blsscls2  15594  metequiv2  15597  bdxmet  15602  mulc1cncf  15690  cncfco  15692  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  lgsdir  16154  lgsquadlem2  16197  2sqlem8a  16241  2sqlem10  16244  uspgrushgr  16421  uspgrupgr  16422  usgruspgr  16424  clwwlkccatlem  16641  lealltlt1  16751  lealltlt2  16752  triap  17078