Theorem sylibr 175

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition.

Hypotheses

Ref	Expression
sylibr.1	⊢ (φ → ψ)
sylibr.2	⊢ (χ ↔ ψ)

Assertion

Ref	Expression
sylibr	⊢ (φ → χ)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 ⊢ (φ → ψ)
2		sylibr.2	. . 3 ⊢ (χ ↔ ψ)
3	2	biimpr 134	. 2 ⊢ (ψ → χ)
4	1, 3	syl 12	1 ⊢ (φ → χ)

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  3imtr4 192  orrd 203  jca 236  imp3a 279  impbid 397  bicon4d 402  bicon2d 404  pm5.74rd 446  ibd 451  oibabs 493  pm5.18 497  ecase2d 558  3mix1 600  3mix2 601  3jca 604  ecased 643  19.8a 712  excomim 727  19.23ai 746  19.29 752  19.39 761  19.24 762  19.34 772  hbim1 781  eqs4 831  a4c 843  a4c1 844  sb2 859  sbequ1 863  sbn2 881  sbea4 894  mo 1020  eu2 1023  exmo 1042  2euex 1061  bm1.1 1088  cleqrd 1100  biabd 1182  biabrdv 1184  biabldv 1185  ra4e 1244  rgen2 1248  r19.21ai 1258  r19.29 1295  elisset 1354  cgsex2g 1368  cgsex4g 1369  cla4e2gv 1398  cla4ev 1401  rcla4ev 1403  ceqex 1410  mo2icl 1434  sbcie 1455  elrabsf 1456  ssrdv 1509  eqssd 1518  syl5ss 1544  pssn2lp 1571  psstr 1574  reuss 1577  reuhyp 1581  ssun1 1621  vss 1729  minel 1743  disjsn 1836  disjsn2 1837  tpi1 1843  tpi2 1844  tpi3 1845  opprc3 1908  opthwiener 1914  elunii 1924  uniss 1936  uniss2 1942  unidif 1943  ssunieq 1945  unisseq 1946  reuuni4 1959  pwuni 1961  intmin 1982  iunss1 2002  ssiun2 2019  iunss2 2021  iunpw 2040  trin 2051  3brtr4g 2088  opelopabg 2115  ssopab2 2119  sotric 2148  so 2152  supeu 2158  supcl 2159  supsn 2168  frirr 2176  tz7.2 2183  epfrc 2185  dfwe2 2187  wereu 2197  ordelord 2221  ordsseleq 2227  ordtri3or 2230  ordtri1 2231  orddisj 2236  ordon 2238  tfi 2244  ssorduni 2249  onint0 2262  suceloni 2314  ordnbtwn 2316  ordsucss 2320  ordsucelsuc 2324  ordzsl 2366  dflim3 2368  omsson 2377  ordom 2382  omssnlim 2386  peano5 2394  xpex 2488  cnvss 2512  opeldm 2534  brelrn 2559  dmcosseq 2572  dmresexg 2586  relssres 2596  resexg 2597  cotr 2625  dminss 2648  imainss 2649  cores 2659  relssdr 2668  funeu 2685  dffun7 2688  funco 2696  funun 2700  fununi 2705  funcnvuni 2706  funimaexg 2715  fnssres 2734  fn0 2739  zfrep6 2744  fnopabg 2745  fss 2759  fco 2760  fssres 2764  feu 2767  fcnvres 2768  f00 2773  fconst 2774  f1co 2783  fores 2794  f1o2 2804  f1o3 2805  f1f1orn 2810  f1oun 2815  f1oco 2816  fv3 2839  tz6.12-1 2842  fvrn 2888  fopab2 2891  ffnfv 2892  fsn 2895  abrexex 2912  f1oiso 2942  iunon 2947  iinon 2948  tfrlem8 2956  tfrlem10 2958  tfrlem11 2959  tfr3 2964  tz7.44-3 2968  tz7.48lem 2993  tz7.48-1 2994  tz7.49 2997  tz7.49c 2998  abianfp 3000  eloprabg 3035  fnoprab 3038  ndmoprass 3062  ndmoprdistr 3063  oawordeulem 3156  oalimcl 3162  omsmo 3196  ecexg 3204  erdisj 3223  ecelqsi 3229  ecopqsi 3230  ecopoprtrn 3247  eceqopreq 3249  th3qlem1 3250  map0b 3267  mapsn 3269  mapss 3270  relsdom 3279  en2d 3303  dom2d 3307  ssdomg 3311  xpdom2 3345  pw2en 3348  sbthlem2 3350  sbthlem3 3351  sbthlem7 3355  sbthlem8 3356  mapenlem2 3385  mapdom2lem 3388  mapxpen 3390  xpmapenlem4 3394  mapunen 3397  limenpsi 3400  php2 3410  php3 3411  ominf 3423  pssnn 3428  ssfi 3430  unblem1 3431  unblem2 3432  unfilem3 3440  unfi2 3442  inf3lem3 3466  inf3lem6 3469  isfinite 3480  nnsdom 3481  infensuc 3484  trcl 3489  setind 3492  r1tr 3498  r1ord 3499  r1val1 3502  tz9.12lem1 3503  tz9.12lem3 3505  tz9.13 3507  rankon 3515  r1pw 3529  rankr1id 3539  scottex 3541  scott0 3542  aceq5 3563  aceq6a 3564  aceq6b 3565  ac6lem 3575  kmlem4 3583  kmlem6 3585  kmlem12 3591  kmlem13 3592  zornlem4 3606  zornlem6 3608  zorn2 3612  fodom 3613  fodomb 3615  htalem 3618  oncardval 3626  oncardon 3627  oncardid 3628  carden 3638  cardsn 3640  entri 3645  entri2 3646  cardlim 3657  cardsdomel 3658  ondomon 3662  ondomcard 3663  cardmin 3666  alephnbtwn 3674  cfub 3703  cflim 3704  cardcf 3706  cflecard 3707  cfsuc 3709  cfom 3710  zfcndext 3759  zfcndrep 3760  addclpi 3814  mulclpi 3815  enqeceq 3841  addclpq 3852  mulclpq 3854  recmulpq 3864  prnmadd 3894  genpn0 3900  genpnnp 3902  genpcl 3905  1pr 3911  psslinpr 3929  prlem934 3933  ltexprlem1 3936  ltexprlem4 3939  ltexprlem5 3940  ltexprlem7 3942  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  enreceq 3971  addclsr 3986  mulclsr 3987  mulgt0sr 4008  suppsr3 4018  axaddcl 4066  axaddrcl 4067  axmulcl 4068  axmulrcl 4069  axnegex 4078  axrnegex 4080  axcnre 4087  axsup 4088  negclt 4141  recdivt 4270  gt0ne0 4340  sqge0 4344  divgt0lem 4389  nn1suc 4435  nnne0t 4444  nnleltp1t 4448  nnsub 4450  creur 4532  creui 4533  nnnegz 4566  elnnz 4572  elnnz1 4581  sqznn 4600  uzwo2 4606  uzwo3lem1 4614  uzwo3lem2 4615  zmin 4617  znq 4630  qaddclt 4642  qnegclt 4643  qmulclt 4644  qrecclt 4646  seqrn 4673  discrlem2 4714  discrlem3 4715  sqrlem5 4735  sqr2irrlem1 4777  replimt 4798  ruclem8 4892  infxpidmlem3 4935  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem11 4943  infdif 4948  infmap2lem2 4952  bcs 5101  hlimreu 5145  hlimeu 5146  chsscm 5147  hsn0elch 5155  ocsh 5164  occont 5168  occl 5188  projlem4 5196  projlem6 5198  projlem10 5202  projlem25 5217  projlem26 5218  projlem28 5220  projlem29 5221  pjthlem2 5226  pjthlem3 5227  pjthlem4 5228  pjthlem14 5238  pjthu 5241  pjthu2 5242  pjoc1 5268  pjoml 5271  choc0 5291  choc1 5292  shintcl 5294  ococint 5298  hsupval2t 5301  spanclt 5305  hsupclt 5308  hsupss 5310  chsupsn 5313  spanss 5319  chlejb1 5397  chabs2t 5433  spanun 5450  spansn 5462  spanunsn 5482  cmbr3 5509  cmbr4 5510  osumlem5 5534  osum 5538  5oalem1 5544  5oalem2 5545  5oalem4 5547  5oalem5 5548  3oalem2 5553  pjss2 5571  pjjs 5585  pjss2co 5634  pjnormss 5638  pjclem4 5653  pjc 5654  pj3s 5659  strlem1 5691  strlem3a 5693  h1dat 5747  chpssat 5756  mdsymlem6 5781  sumdmdi 5785  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org