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  3082  opeldmg  4981  elreldm  5003  ssimaex  5758  resflem  5863  f1eqcocnv  5987  fliftfun  5992  isopolem  6018  isosolem  6020  brtposg  6515  issmo2  6550  nnmcl  6744  nnawordi  6778  nnmordi  6779  nnmord  6780  swoord1  6826  ecopovtrn  6896  ecopovtrng  6899  f1domg  7034  mapen  7136  mapxpen  7138  mapunen  7141  supmoti  7323  isotilem  7336  exmidomniim  7471  enq0tr  7791  prubl  7843  ltexprlemloc  7964  addextpr  7978  recexprlem1ssl  7990  recexprlem1ssu  7991  cauappcvgprlemdisj  8008  mulcmpblnr  8098  mulgt0sr  8135  map2psrprg  8162  ltleletr  8397  ltle  8403  ltadd2  8737  leltadd  8765  reapti  8897  apreap  8905  reapcotr  8916  apcotr  8925  addext  8928  mulext1  8930  zapne  9698  zextle  9716  prime  9724  uzin  9934  indstr  9972  supinfneg  9974  infsupneg  9975  ublbneg  9992  xrltle  10179  xrre2  10202  icc0r  10307  fzrevral  10490  flqge  10695  modqadd1  10776  modqmul1  10792  facdiv  11154  elfzelfzccat  11346  resqrexlemgt0  11764  abs00ap  11806  absext  11807  climshftlemg  12046  climcaucn  12095  dvds2lem  12548  dvdsfac  12605  ltoddhalfle  12638  ndvdsadd  12676  bitsinv1lem  12706  gcdaddm  12739  bezoutlembi  12760  gcdzeq  12777  algcvga  12807  rpdvds  12855  cncongr1  12859  cncongr2  12860  prmind2  12876  euclemma  12902  isprm6  12903  rpexp  12909  sqrt2irr  12918  odzdvds  13002  pclemub  13044  pceulem  13051  pc2dvds  13087  fldivp1  13105  infpnlem1  13116  prmunb  13119  ballotfilem7  13257  issubg4m  13973  imasabl  14117  fiinbas  15073  bastg  15085  tgcl  15088  opnssneib  15180  tgcnp  15233  iscnp4  15242  cnntr  15249  cnptopresti  15262  lmss  15270  lmtopcnp  15274  txdis  15301  xblss2ps  15428  xblss2  15429  blsscls2  15517  metequiv2  15520  bdxmet  15525  mulc1cncf  15613  cncfco  15615  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  lgsdir  16068  lgsquadlem2  16111  2sqlem8a  16155  2sqlem10  16158  uspgrushgr  16335  uspgrupgr  16336  usgruspgr  16338  clwwlkccatlem  16555  lealltlt1  16665  lealltlt2  16666  triap  16983