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  2991  opeldmg  4825  elreldm  4846  ssimaex  5569  resflem  5672  f1eqcocnv  5782  fliftfun  5787  isopolem  5813  isosolem  5815  brtposg  6245  issmo2  6280  nnmcl  6472  nnawordi  6506  nnmordi  6507  nnmord  6508  swoord1  6554  ecopovtrn  6622  ecopovtrng  6625  f1domg  6748  mapen  6836  mapxpen  6838  supmoti  6982  isotilem  6995  exmidomniim  7129  enq0tr  7408  prubl  7460  ltexprlemloc  7581  addextpr  7595  recexprlem1ssl  7607  recexprlem1ssu  7608  cauappcvgprlemdisj  7625  mulcmpblnr  7715  mulgt0sr  7752  map2psrprg  7779  ltleletr  8013  ltle  8019  ltadd2  8350  leltadd  8378  reapti  8510  apreap  8518  reapcotr  8529  apcotr  8538  addext  8541  mulext1  8543  zapne  9298  zextle  9315  prime  9323  uzin  9531  indstr  9564  supinfneg  9566  infsupneg  9567  ublbneg  9584  xrltle  9767  xrre2  9790  icc0r  9895  fzrevral  10073  flqge  10250  modqadd1  10329  modqmul1  10345  facdiv  10684  resqrexlemgt0  10995  abs00ap  11037  absext  11038  climshftlemg  11276  climcaucn  11325  dvds2lem  11776  dvdsfac  11831  ltoddhalfle  11863  ndvdsadd  11901  gcdaddm  11950  bezoutlembi  11971  gcdzeq  11988  algcvga  12016  rpdvds  12064  cncongr1  12068  cncongr2  12069  prmind2  12085  euclemma  12111  isprm6  12112  rpexp  12118  sqrt2irr  12127  odzdvds  12210  pclemub  12252  pceulem  12259  pc2dvds  12294  fldivp1  12311  infpnlem1  12322  prmunb  12325  fiinbas  13098  bastg  13112  tgcl  13115  opnssneib  13207  tgcnp  13260  iscnp4  13269  cnntr  13276  cnptopresti  13289  lmss  13297  lmtopcnp  13301  txdis  13328  xblss2ps  13455  xblss2  13456  blsscls2  13544  metequiv2  13547  bdxmet  13552  mulc1cncf  13627  cncfco  13629  sincosq2sgn  13799  sincosq3sgn  13800  sincosq4sgn  13801  lgsdir  13987  2sqlem8a  14009  2sqlem10  14012  triap  14318