Theorem sylbir 224

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.)

Hypotheses

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

Assertion

Ref	Expression
sylbir	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 217	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 195

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

This theorem depends on definitions:  df-bi 196

This theorem is referenced by:  3imtr3i  279  ex  449  3ori  1380  19.38  1757  19.35  1794  equsex  2281  nfeqf2  2285  sbi2  2381  mo2v  2465  2mo  2539  axie2  2585  necon1bi  2810  necon1i  2815  sbhypf  3226  vtocl2  3234  vtocl3  3235  reu6  3362  uneqin  3837  difin0ss  3900  inelcm  3984  difprsn1  4271  tppreqb  4277  n0snor2el  4304  unissint  4436  intminss  4438  iununi  4546  bm1.3ii  4712  eusv2nf  4790  reusv3i  4801  reuxfr2d  4817  moabex  4854  copsex2g  4884  opelopabt  4912  eqrelrel  5144  opeliunxp2  5182  opelrn  5278  issref  5428  ssxpb  5487  xpima  5495  xpimasn  5498  dmsn0el  5522  relcoi2  5580  elsnxp  5594  elsnxpOLD  5595  iotanul  5783  dffv2  6181  fnfvrnss  6297  fressnfv  6332  fconst5  6376  f1mpt  6419  isocnv3  6482  f1owe  6503  ovprc  6581  onminesb  6890  onminsb  6891  onintrab  6893  onnminsb  6896  onsucuni2  6926  tfindsg2  6953  zfrep6  7027  fo1stres  7083  fo2ndres  7084  bropopvvv  7142  bropfvvvv  7144  frxp  7174  opeliunxp2f  7223  mpt2xopoveqd  7234  reldmtpos  7247  wfrlem4  7305  wfrlem12  7313  wfrlem16  7317  wfr2  7321  tfrlem5  7363  tfrlem9  7368  tfr2  7381  rdgsuc  7407  oaordi  7513  oeordi  7554  omopthi  7624  fvmptmap  7780  mptelixpg  7831  ener  7888  enerOLD  7889  domtr  7895  snfi  7923  unen  7925  xpf1o  8007  mapen  8009  unxpdomlem3  8051  isinf  8058  frfi  8090  unblem1  8097  unfi  8112  fofinf1o  8126  fsuppun  8177  inf3lem2  8409  inf3lem5  8412  cantnfp1lem1  8458  cantnfp1lem3  8460  tcmin  8500  r1ordg  8524  r1ord  8526  rankr1ai  8544  r1val3  8584  bndrank  8587  unbndrank  8588  rankr1b  8610  rankxplim3  8627  tcrank  8630  xpnum  8660  cardmin2  8707  infxpenlem  8719  fseqen  8733  dfac8clem  8738  alephsson  8806  alephfp  8814  dfac4  8828  kmlem6  8860  kmlem8  8862  kmlem9  8863  infpssr  9013  fin1a2lem12  9116  axcc4  9144  axcc4dom  9146  ac6s2  9191  zornn0g  9210  cardidg  9249  unsnen  9254  pwcfsdom  9284  cfpwsdom  9285  gchpwdom  9371  r1tskina  9483  intgru  9515  indpi  9608  nqereu  9630  supsrlem  9811  letrii  10041  dfnn3  10911  zaddcl  11294  nn0ind  11348  fnn0ind  11352  ublbneg  11649  nn01to3  11657  infmrp1  12045  fz0  12227  fzo1fzo0n0  12386  elfzom1elp1fzo  12402  fzo0end  12426  elfznelfzo  12439  fzind2  12448  injresinjlem  12450  fleqceilz  12515  nnsinds  12649  nn0sinds  12650  faclbnd4lem1  12942  hashinf  12984  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashgt0elex  13050  hashfacen  13095  hash2prde  13109  hash2sspr  13124  fun2dmnop0  13131  swrdn0  13282  swrdlsw  13304  swrdswrdlem  13311  swrdccatin12lem3  13341  swrdccat3  13343  swrdccat3blem  13346  cshwsublen  13393  cshwidxmod  13400  repswcshw  13409  cshw1  13419  trclun  13603  dmtrclfv  13607  rediv  13719  imdiv  13726  sqrt0  13830  fsump1i  14342  modfsummods  14366  bpolydiflem  14624  bpoly3  14628  bpoly4  14629  cos1bnd  14756  sinltx  14758  rpnnen2lem1  14782  rpnnen2lem2  14783  rpnnen2lem12  14793  odd2np1  14903  opoe  14925  omoe  14926  opeo  14927  omeo  14928  gcdcllem1  15059  gcdaddmlem  15083  dfgcd2  15101  algfx  15131  lcmledvds  15150  lcmfunsnlem  15192  lcmfun  15196  coprmprod  15213  coprmproddvdslem  15214  prmn2uzge3OLD  15251  odzval  15334  odzdvds  15338  prmreclem5  15462  mul4sq  15496  prmgaplem5  15597  prmgaplem6  15598  imasaddfnlem  16011  mreexexlem4d  16130  joindmss  16830  meetdmss  16844  gictr  17540  cntzval  17577  symg2bas  17641  efgsfo  17975  efgrelexlemb  17986  dprddomcld  18223  dprdsubg  18246  dprd2da  18264  lssacs  18788  cnfldinv  19596  ocvval  19830  dmatmul  20122  mdetfval1  20215  mndifsplit  20261  fvmptnn04if  20473  opnnei  20734  ordtbas2  20805  ordtrest2lem  20817  lmmo  20994  fincmp  21006  bwth  21023  txbas  21180  ptcnplem  21234  tx2ndc  21264  hmphtr  21396  fbun  21454  filcon  21497  ptcmplem5  21670  cnextcn  21681  utoptop  21848  ucncn  21899  metust  22173  cfilucfil  22174  elcncf1di  22506  xrhmeo  22553  phtpycc  22598  copco  22626  pcohtpylem  22627  pcopt  22630  pcopt2  22631  ncvsi  22759  ovolval  23049  iunmbl2  23132  itg2splitlem  23321  cpnfval  23501  plyval  23753  fta1  23867  aaliou2b  23900  tayl0  23920  ulmdvlem3  23960  radcnvlem2  23972  dvradcnv  23979  reeff1o  24005  sincosq1lem  24053  sincosq2sgn  24055  sincosq4sgn  24057  sinq12ge0  24064  logrncl  24118  eflog  24127  cxpge0  24229  logb1  24307  atanf  24407  atanbnd  24453  igamf  24577  igamcl  24578  lgsne0  24860  mul2sq  24944  pntibnd  25082  ostth  25128  mptelee  25575  axlowdimlem9  25630  axlowdimlem12  25633  axcontlem2  25645  axcontlem12  25655  structgrssvtx  25701  structgrssiedg  25702  lpvtx  25734  isusgra0  25876  usgraop  25879  usgraedg4  25916  nbusgra  25957  nbgranself2  25965  wlkn0  26055  wlkcpr  26057  wlkntrllem3  26091  spthonepeq  26117  wlkdvspth  26138  cyclnspth  26159  3v3e3cycl2  26192  3v3e3cycl  26193  4cycl4dv  26195  2wlkeq  26235  usg2wlkeq  26236  clwwlknprop  26300  clwwisshclww  26335  wlklenvclwlk  26366  2wlkonot3v  26402  2spthonot3v  26403  2spontn0vne  26414  vdgrf  26425  usgfiregdegfi  26438  nbhashuvtx1  26442  eupath2lem1  26504  frgra3vlem1  26527  frgra3vlem2  26528  frgrancvvdeqlem2  26558  frgrancvvdeqlem3  26559  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  frgrawopreglem5  26575  usgreghash2spot  26596  numclwwlk5  26639  frgrareg  26644  frgraregord013  26645  friendshipgt3  26648  isgrpo  26735  vciOLD  26800  vcex  26817  nmogtmnf  27009  siilem1  27090  siii  27092  ajmoi  27098  bcsiALT  27420  hhcms  27444  ocval  27523  hsupval  27577  omlsilem  27645  h1de2bi  27797  h1de2ctlem  27798  hosubeq0i  28069  adjmo  28075  nmopgtmnf  28111  nlfnval  28124  nmcopex  28272  nmcfnex  28296  riesz4i  28306  riesz1  28308  riesz2  28309  opsqrlem1  28383  superpos  28597  hatomistici  28605  chpssati  28606  mdsymlem3  28648  3o1cs  28693  3o2cs  28694  3o3cs  28695  spc2ed  28696  brabgaf  28800  f1mptrn  28816  ffsrn  28892  fpwrelmap  28896  ordtrest2NEWlem  29296  qqhval2  29354  esumfsup  29459  esumcvg  29475  cntnevol  29618  ddemeas  29626  dya2icoseg2  29667  dya2iocnei  29671  eulerpartlems  29749  eulerpartlemgvv  29765  eulerpart  29771  cndprobprob  29827  ballotlemsdom  29900  ballotth  29926  sgn3da  29930  bnj945  30098  bnj1379  30155  bnj1459  30167  bnj557  30225  bnj571  30230  bnj849  30249  bnj964  30267  bnj978  30273  bnj1018  30286  bnj1020  30287  bnj1033  30291  bnj1175  30326  bnj1398  30356  bnj1417  30363  bnj1523  30393  txpcon  30468  msubco  30682  mclsax  30720  setinds  30927  dfon2lem7  30938  dfon2lem8  30939  poseq  30994  soseq  30995  frrlem4  31027  frrlem11  31036  nodenselem4  31083  nocvxminlem  31089  nocvxmin  31090  pprodss4v  31161  fullfunfv  31224  altxpsspw  31254  funtransport  31308  fvtransport  31309  funray  31417  fvray  31418  funline  31419  fvline  31421  finminlem  31482  bisym1  31588  onsucconi  31606  onsucsuccmpi  31612  bj-alcomexcom  31857  axc11n11r  31860  bj-equsal2  32000  bj-xpima1snALT  32137  mptsnunlem  32361  iooelexlt  32386  relowlpssretop  32388  rdgeqoa  32394  wl-dveeq12  32490  wl-lem-nexmo  32528  matunitlindflem1  32575  ptrecube  32579  poimirlem26  32605  poimirlem30  32609  poimir  32612  ismblfin  32620  itg2addnclem  32631  dvasin  32666  sdclem2  32708  totbndbnd  32758  ismgmOLD  32819  exidresid  32848  isrngo  32866  rngoablo2  32878  rngoueqz  32909  isdivrngo  32919  isdrngo1  32925  isdrngo2  32927  ispridl2  33007  prtlem11  33169  ax12eq  33244  ax12el  33245  lkr0f  33399  hl2at  33709  dalemswapyz  33960  pclfinclN  34254  osumcllem11N  34270  pexmidlem8N  34281  ltrnnid  34440  mptfcl  36301  fphpd  36398  elmnc  36725  itgoval  36750  arearect  36820  clsk3nimkb  37358  nanorxor  37526  pm11.71  37619  iotavalsb  37656  sbiota1  37657  2uasbanh  37798  eel0TT  37950  eelT00  37951  eelTTT  37952  eelT11  37953  eelT12  37955  eelTT1  37956  eelT01  37957  eel0T1  37958  eelTT  38019  uunT1p1  38029  uun121  38031  uun121p1  38032  un2122  38038  uunTT1  38041  uunTT1p1  38042  uunTT1p2  38043  uunT11  38044  uunT11p1  38045  uunT11p2  38046  uunT12  38047  uunT12p1  38048  uunT12p2  38049  uunT12p3  38050  uunT12p4  38051  uunT12p5  38052  uun111  38053  3anidm12p2  38055  uun123  38056  3impdirp1  38064  undif3VD  38140  ax6e2ndeqVD  38167  2uasbanhVD  38169  ax6e2ndeqALT  38189  iunconlem2  38193  sineq0ALT  38195  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem3  38896  stoweidlem17  38910  fourierdlem42  39042  fourierdlem48  39047  fourierdlem50  39049  fourierdlem51  39050  fourierdlem76  39075  fourierdlem83  39082  fourierdlem87  39086  hoidmvval0  39477  rexrsb  39818  raaan2  39824  afv0nbfvbi  39880  afvfv0bi  39881  afveu  39882  fnbrafvb  39883  afvres  39901  tz6.12-afv  39902  dmfcoafv  39904  afvco2  39905  aovprc  39917  aovrcl  39918  aovmpt4g  39930  fzopred  39945  lighneal  40066  pfxccat3  40289  pfxccat3a  40292  falseral0  40308  2ffzoeq  40361  nbuhgr  40565  nbumgr  40569  nbuhgr2vtx1edgblem  40573  nbgr0vtxlem  40577  nbgr1vtx  40580  uvtxa01vtx0  40623  cusgrsizeinds  40668  sizusglecusglem2  40678  uhgrvd00  40750  fusgrregdegfi  40769  rusgr1vtxlem  40787  1wlkeq  40838  1wlk1walk  40843  upgr1wlkwlk  40847  uspgr2wlkeq  40854  1wlklenvclwlk  40863  1wlkreslem  40878  1wlkdlem2  40892  1wlkdlem4  40894  spthonepeq-av  40958  clwwisshclwws  41235  31wlkdlem6  41332  eupth2eucrct  41385  eupth2lem1  41386  eupth2lem3lem7  41402  frgr3vlem1  41443  frgr3vlem2  41444  frgrncvvdeqlem2  41470  frgrncvvdeqlem3  41471  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  frgrwopreglem5  41485  fusgreghash2wsp  41502  av-numclwwlk5  41542  av-frgrareg  41548  av-frgraregord013  41549  av-friendshipgt3  41552  ovn0ssdmfun  41557  islinindfis  42032  setrec2fun  42238  elsetrecslem  42243  secval  42287  cscval  42288  cotval  42289