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  4988  elreldm  5010  ssimaex  5767  resflem  5875  f1eqcocnv  6000  fliftfun  6005  isopolem  6031  isosolem  6033  brtposg  6530  issmo2  6565  nnmcl  6759  nnawordi  6793  nnmordi  6794  nnmord  6795  swoord1  6841  ecopovtrn  6911  ecopovtrng  6914  f1domg  7050  mapen  7152  mapxpen  7154  mapunen  7157  supmoti  7339  isotilem  7352  exmidomniim  7487  enq0tr  7807  prubl  7859  ltexprlemloc  7980  addextpr  7994  recexprlem1ssl  8006  recexprlem1ssu  8007  cauappcvgprlemdisj  8024  mulcmpblnr  8114  mulgt0sr  8151  map2psrprg  8178  ltleletr  8413  ltle  8419  ltadd2  8754  leltadd  8782  reapti  8915  apreap  8923  reapcotr  8934  apcotr  8943  addext  8946  mulext1  8948  zapne  9728  zextle  9747  prime  9755  uzin  9970  indstr  10008  supinfneg  10010  infsupneg  10011  ublbneg  10028  xrltle  10216  xrre2  10239  icc0r  10344  fzrevral  10528  flqge  10735  flapge  10736  modqadd1  10818  modqmul1  10834  facdiv  11197  elfzelfzccat  11389  resqrexlemgt0  11807  abs00ap  11849  absext  11850  climshftlemg  12092  climcaucn  12141  dvds2lem  12594  dvdsfac  12651  ltoddhalfle  12684  ndvdsadd  12722  bitsinv1lem  12752  gcdaddm  12785  bezoutlembi  12806  gcdzeq  12823  algcvga  12853  rpdvds  12901  cncongr1  12905  cncongr2  12906  prmind2  12922  euclemma  12949  isprm6  12950  rpexp  12956  sqrt2irr  12965  odzdvds  13052  pclemub  13094  pceulem  13101  pc2dvds  13137  fldivp1  13155  infpnlem1  13166  prmunb  13169  ballotfilem7  13336  issubg4m  14054  imasabl  14229  fiinbas  15292  bastg  15304  tgcl  15307  opnssneib  15399  tgcnp  15452  iscnp4  15461  cnntr  15468  cnptopresti  15481  lmss  15489  lmtopcnp  15493  txdis  15520  xblss2ps  15647  xblss2  15648  blsscls2  15736  metequiv2  15739  bdxmet  15744  mulc1cncf  15832  cncfco  15834  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  chtublem  16312  chtqub  16313  bposlem1  16328  bposlem3  16330  bposlem7  16334  lgsdir  16376  lgsquadlem2  16419  2sqlem8a  16463  2sqlem10  16466  uspgrushgr  16643  uspgrupgr  16644  usgruspgr  16646  clwwlkccatlem  16863  lealltlt1  16973  lealltlt2  16974  triap  17301