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  8748  leltadd  8776  reapti  8909  apreap  8917  reapcotr  8928  apcotr  8937  addext  8940  mulext1  8942  zapne  9723  zextle  9741  prime  9749  uzin  9964  indstr  10002  supinfneg  10004  infsupneg  10005  ublbneg  10022  xrltle  10210  xrre2  10233  icc0r  10338  fzrevral  10522  flqge  10729  flapge  10730  modqadd1  10811  modqmul1  10827  facdiv  11190  elfzelfzccat  11382  resqrexlemgt0  11800  abs00ap  11842  absext  11843  climshftlemg  12084  climcaucn  12133  dvds2lem  12586  dvdsfac  12643  ltoddhalfle  12676  ndvdsadd  12714  bitsinv1lem  12744  gcdaddm  12777  bezoutlembi  12798  gcdzeq  12815  algcvga  12845  rpdvds  12893  cncongr1  12897  cncongr2  12898  prmind2  12914  euclemma  12941  isprm6  12942  rpexp  12948  sqrt2irr  12957  odzdvds  13044  pclemub  13086  pceulem  13093  pc2dvds  13129  fldivp1  13147  infpnlem1  13158  prmunb  13161  ballotfilem7  13328  issubg4m  14045  imasabl  14189  fiinbas  15199  bastg  15211  tgcl  15214  opnssneib  15306  tgcnp  15359  iscnp4  15368  cnntr  15375  cnptopresti  15388  lmss  15396  lmtopcnp  15400  txdis  15427  xblss2ps  15554  xblss2  15555  blsscls2  15643  metequiv2  15646  bdxmet  15651  mulc1cncf  15739  cncfco  15741  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  bposlem1  16209  bposlem3  16211  lgsdir  16252  lgsquadlem2  16295  2sqlem8a  16339  2sqlem10  16342  uspgrushgr  16519  uspgrupgr  16520  usgruspgr  16522  clwwlkccatlem  16739  lealltlt1  16849  lealltlt2  16850  triap  17176