Theorem sylibrd 168

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibrd.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
sylibrd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  sbciegft  2905  opeldmg  4702  elreldm  4723  ssimaex  5434  resflem  5536  f1eqcocnv  5644  fliftfun  5649  isopolem  5675  isosolem  5677  brtposg  6103  issmo2  6138  nnmcl  6329  nnawordi  6363  nnmordi  6364  nnmord  6365  swoord1  6410  ecopovtrn  6478  ecopovtrng  6481  f1domg  6604  mapen  6691  mapxpen  6693  supmoti  6830  isotilem  6843  exmidomniim  6961  enq0tr  7184  prubl  7236  ltexprlemloc  7357  addextpr  7371  recexprlem1ssl  7383  recexprlem1ssu  7384  cauappcvgprlemdisj  7401  mulcmpblnr  7478  mulgt0sr  7514  ltleletr  7763  ltle  7768  ltadd2  8094  leltadd  8122  reapti  8253  apreap  8261  reapcotr  8272  apcotr  8281  addext  8284  mulext1  8286  cnstab  8318  zapne  9023  zextle  9040  prime  9048  uzin  9254  indstr  9284  supinfneg  9286  infsupneg  9287  ublbneg  9301  xrltle  9471  xrre2  9491  icc0r  9596  fzrevral  9772  flqge  9942  modqadd1  10021  modqmul1  10037  facdiv  10371  resqrexlemgt0  10678  abs00ap  10720  absext  10721  climshftlemg  10957  climcaucn  11006  dvds2lem  11347  dvdsfac  11400  ltoddhalfle  11432  ndvdsadd  11470  gcdaddm  11514  bezoutlembi  11533  gcdzeq  11550  algcvga  11572  rpdvds  11620  cncongr1  11624  cncongr2  11625  prmind2  11641  euclemma  11664  isprm6  11665  rpexp  11671  sqrt2irr  11680  fiinbas  12053  bastg  12067  tgcl  12070  opnssneib  12162  tgcnp  12214  iscnp4  12223  cnntr  12230  cnptopresti  12243  lmss  12251  lmtopcnp  12255  txdis  12282  xblss2ps  12387  xblss2  12388  blsscls2  12476  metequiv2  12479  bdxmet  12484  mulc1cncf  12556  cncfco  12558  triap  12905