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  2995  opeldmg  4834  elreldm  4855  ssimaex  5579  resflem  5682  f1eqcocnv  5794  fliftfun  5799  isopolem  5825  isosolem  5827  brtposg  6257  issmo2  6292  nnmcl  6484  nnawordi  6518  nnmordi  6519  nnmord  6520  swoord1  6566  ecopovtrn  6634  ecopovtrng  6637  f1domg  6760  mapen  6848  mapxpen  6850  supmoti  6994  isotilem  7007  exmidomniim  7141  enq0tr  7435  prubl  7487  ltexprlemloc  7608  addextpr  7622  recexprlem1ssl  7634  recexprlem1ssu  7635  cauappcvgprlemdisj  7652  mulcmpblnr  7742  mulgt0sr  7779  map2psrprg  7806  ltleletr  8041  ltle  8047  ltadd2  8378  leltadd  8406  reapti  8538  apreap  8546  reapcotr  8557  apcotr  8566  addext  8569  mulext1  8571  zapne  9329  zextle  9346  prime  9354  uzin  9562  indstr  9595  supinfneg  9597  infsupneg  9598  ublbneg  9615  xrltle  9800  xrre2  9823  icc0r  9928  fzrevral  10107  flqge  10284  modqadd1  10363  modqmul1  10379  facdiv  10720  resqrexlemgt0  11031  abs00ap  11073  absext  11074  climshftlemg  11312  climcaucn  11361  dvds2lem  11812  dvdsfac  11868  ltoddhalfle  11900  ndvdsadd  11938  gcdaddm  11987  bezoutlembi  12008  gcdzeq  12025  algcvga  12053  rpdvds  12101  cncongr1  12105  cncongr2  12106  prmind2  12122  euclemma  12148  isprm6  12149  rpexp  12155  sqrt2irr  12164  odzdvds  12247  pclemub  12289  pceulem  12296  pc2dvds  12331  fldivp1  12348  infpnlem1  12359  prmunb  12362  issubg4m  13058  fiinbas  13634  bastg  13646  tgcl  13649  opnssneib  13741  tgcnp  13794  iscnp4  13803  cnntr  13810  cnptopresti  13823  lmss  13831  lmtopcnp  13835  txdis  13862  xblss2ps  13989  xblss2  13990  blsscls2  14078  metequiv2  14081  bdxmet  14086  mulc1cncf  14161  cncfco  14163  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  lgsdir  14521  2sqlem8a  14554  2sqlem10  14557  triap  14862