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  3082  opeldmg  4984  elreldm  5006  ssimaex  5761  resflem  5866  f1eqcocnv  5991  fliftfun  5996  isopolem  6022  isosolem  6024  brtposg  6519  issmo2  6554  nnmcl  6748  nnawordi  6782  nnmordi  6783  nnmord  6784  swoord1  6830  ecopovtrn  6900  ecopovtrng  6903  f1domg  7038  mapen  7140  mapxpen  7142  mapunen  7145  supmoti  7327  isotilem  7340  exmidomniim  7475  enq0tr  7795  prubl  7847  ltexprlemloc  7968  addextpr  7982  recexprlem1ssl  7994  recexprlem1ssu  7995  cauappcvgprlemdisj  8012  mulcmpblnr  8102  mulgt0sr  8139  map2psrprg  8166  ltleletr  8401  ltle  8407  ltadd2  8741  leltadd  8769  reapti  8901  apreap  8909  reapcotr  8920  apcotr  8929  addext  8932  mulext1  8934  zapne  9702  zextle  9720  prime  9728  uzin  9938  indstr  9976  supinfneg  9978  infsupneg  9979  ublbneg  9996  xrltle  10183  xrre2  10206  icc0r  10311  fzrevral  10495  flqge  10700  modqadd1  10781  modqmul1  10797  facdiv  11159  elfzelfzccat  11351  resqrexlemgt0  11769  abs00ap  11811  absext  11812  climshftlemg  12051  climcaucn  12100  dvds2lem  12553  dvdsfac  12610  ltoddhalfle  12643  ndvdsadd  12681  bitsinv1lem  12711  gcdaddm  12744  bezoutlembi  12765  gcdzeq  12782  algcvga  12812  rpdvds  12860  cncongr1  12864  cncongr2  12865  prmind2  12881  euclemma  12907  isprm6  12908  rpexp  12914  sqrt2irr  12923  odzdvds  13007  pclemub  13049  pceulem  13056  pc2dvds  13092  fldivp1  13110  infpnlem1  13121  prmunb  13124  ballotfilem7  13262  issubg4m  13979  imasabl  14123  fiinbas  15133  bastg  15145  tgcl  15148  opnssneib  15240  tgcnp  15293  iscnp4  15302  cnntr  15309  cnptopresti  15322  lmss  15330  lmtopcnp  15334  txdis  15361  xblss2ps  15488  xblss2  15489  blsscls2  15577  metequiv2  15580  bdxmet  15585  mulc1cncf  15673  cncfco  15675  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  lgsdir  16137  lgsquadlem2  16180  2sqlem8a  16224  2sqlem10  16227  uspgrushgr  16404  uspgrupgr  16405  usgruspgr  16407  clwwlkccatlem  16624  lealltlt1  16734  lealltlt2  16735  triap  17052