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  6529  issmo2  6564  nnmcl  6758  nnawordi  6792  nnmordi  6793  nnmord  6794  swoord1  6840  ecopovtrn  6910  ecopovtrng  6913  f1domg  7048  mapen  7150  mapxpen  7152  mapunen  7155  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  9730  zextle  9748  prime  9756  uzin  9971  indstr  10009  supinfneg  10011  infsupneg  10012  ublbneg  10029  xrltle  10217  xrre2  10240  icc0r  10345  fzrevral  10529  flqge  10736  flapge  10737  modqadd1  10819  modqmul1  10835  facdiv  11198  elfzelfzccat  11390  resqrexlemgt0  11808  abs00ap  11850  absext  11851  climshftlemg  12093  climcaucn  12142  dvds2lem  12595  dvdsfac  12652  ltoddhalfle  12685  ndvdsadd  12723  bitsinv1lem  12753  gcdaddm  12786  bezoutlembi  12807  gcdzeq  12824  algcvga  12854  rpdvds  12902  cncongr1  12906  cncongr2  12907  prmind2  12923  euclemma  12950  isprm6  12951  rpexp  12957  sqrt2irr  12966  odzdvds  13053  pclemub  13095  pceulem  13102  pc2dvds  13138  fldivp1  13156  infpnlem1  13167  prmunb  13170  ballotfilem7  13337  issubg4m  14055  imasabl  14230  fiinbas  15275  bastg  15287  tgcl  15290  opnssneib  15382  tgcnp  15435  iscnp4  15444  cnntr  15451  cnptopresti  15464  lmss  15472  lmtopcnp  15476  txdis  15503  xblss2ps  15630  xblss2  15631  blsscls2  15719  metequiv2  15722  bdxmet  15727  mulc1cncf  15815  cncfco  15817  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  chtublem  16295  chtqub  16296  bposlem1  16311  bposlem3  16313  bposlem7  16317  lgsdir  16359  lgsquadlem2  16402  2sqlem8a  16446  2sqlem10  16449  uspgrushgr  16626  uspgrupgr  16627  usgruspgr  16629  clwwlkccatlem  16846  lealltlt1  16956  lealltlt2  16957  triap  17284