Theorem sylibrd 169

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 158	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  3017  opeldmg  4868  elreldm  4889  ssimaex  5619  resflem  5723  f1eqcocnv  5835  fliftfun  5840  isopolem  5866  isosolem  5868  brtposg  6309  issmo2  6344  nnmcl  6536  nnawordi  6570  nnmordi  6571  nnmord  6572  swoord1  6618  ecopovtrn  6688  ecopovtrng  6691  f1domg  6814  mapen  6904  mapxpen  6906  supmoti  7054  isotilem  7067  exmidomniim  7202  enq0tr  7496  prubl  7548  ltexprlemloc  7669  addextpr  7683  recexprlem1ssl  7695  recexprlem1ssu  7696  cauappcvgprlemdisj  7713  mulcmpblnr  7803  mulgt0sr  7840  map2psrprg  7867  ltleletr  8103  ltle  8109  ltadd2  8440  leltadd  8468  reapti  8600  apreap  8608  reapcotr  8619  apcotr  8628  addext  8631  mulext1  8633  zapne  9394  zextle  9411  prime  9419  uzin  9628  indstr  9661  supinfneg  9663  infsupneg  9664  ublbneg  9681  xrltle  9867  xrre2  9890  icc0r  9995  fzrevral  10174  flqge  10354  modqadd1  10435  modqmul1  10451  facdiv  10812  resqrexlemgt0  11167  abs00ap  11209  absext  11210  climshftlemg  11448  climcaucn  11497  dvds2lem  11949  dvdsfac  12005  ltoddhalfle  12037  ndvdsadd  12075  gcdaddm  12124  bezoutlembi  12145  gcdzeq  12162  algcvga  12192  rpdvds  12240  cncongr1  12244  cncongr2  12245  prmind2  12261  euclemma  12287  isprm6  12288  rpexp  12294  sqrt2irr  12303  odzdvds  12386  pclemub  12428  pceulem  12435  pc2dvds  12471  fldivp1  12489  infpnlem1  12500  prmunb  12503  issubg4m  13266  imasabl  13409  fiinbas  14228  bastg  14240  tgcl  14243  opnssneib  14335  tgcnp  14388  iscnp4  14397  cnntr  14404  cnptopresti  14417  lmss  14425  lmtopcnp  14429  txdis  14456  xblss2ps  14583  xblss2  14584  blsscls2  14672  metequiv2  14675  bdxmet  14680  mulc1cncf  14768  cncfco  14770  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  lgsdir  15192  lgsquadlem2  15235  2sqlem8a  15279  2sqlem10  15282  triap  15589