Theorem sylbir 234

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 227	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3i  290  ex  412  3expa  1116  3ori  1422  nanass  1502  19.38  1842  19.35  1881  19.8aw  2054  equsexv  2263  sbi2  2302  nfeqf2  2377  equsex  2418  dfmoeu  2536  2mo  2650  axie2  2704  necon1bi  2971  necon1i  2976  r19.35  3268  sbhypf  3481  spc2ed  3530  reu6  3656  rabssrabd  4012  uneqin  4209  difin0ss  4299  inelcm  4395  rzal  4436  ralf0  4441  falseral0  4447  raaan2  4452  difprsn1  4730  tppreqb  4735  n0snor2el  4761  unissint  4900  intminss  4902  iununi  5024  triin  5202  bm1.3ii  5221  eusv2nf  5313  reusv3i  5322  moabex  5368  copsex2gOLD  5402  opelopabt  5438  eqrelrel  5696  opeliunxp2  5736  opelrn  5841  ssxpb  6066  xpima  6074  xpimasn  6077  dmsn0el  6103  relcnvtr  6160  relcoi2  6169  elsnxp  6183  reuop  6185  iotanul  6396  dffv2  6845  fnfvrnss  6976  fressnfv  7014  fconst5  7063  f1mpt  7115  isocnv3  7183  f1owe  7204  ovprc  7293  fvmpopr2d  7412  onminesb  7620  onminsb  7621  onintrab  7623  onnminsb  7626  onsucuni2  7656  tfindsg2  7683  zfrep6  7771  fo1stres  7830  fo2ndres  7831  bropopvvv  7901  bropfvvvv  7903  frxp  7938  opeliunxp2f  7997  mpoxopoveqd  8008  reldmtpos  8021  frrlem4  8076  wfrlem4OLD  8114  wfrlem12OLD  8122  wfrlem16OLD  8126  wfr2OLD  8130  tfrlem5  8182  tfrlem9  8187  tfr2  8200  rdgsuc  8226  oaordi  8339  oeordi  8380  omopthi  8451  fvmptmap  8627  mptelixpg  8681  ener  8742  domtr  8748  snfi  8788  unen  8790  xpf1o  8875  mapen  8877  rexdif1en  8906  dif1en  8907  pssnn  8913  unfi  8917  ssfi  8918  ensymfib  8930  entrfil  8931  enfii  8932  domtrfi  8938  unxpdomlem3  8958  isinf  8965  frfi  8989  unblem1  8996  unfiOLD  9011  fofinf1o  9024  fsuppun  9077  inf3lem2  9317  inf3lem5  9320  cantnfp1lem1  9366  cantnfp1lem3  9368  tcmin  9430  frr2  9449  r1ordg  9467  r1ord  9469  rankr1ai  9487  r1val3  9527  bndrank  9530  unbndrank  9531  rankr1b  9553  rankxplim3  9570  tcrank  9573  xpnum  9640  cardmin2  9688  infxpenlem  9700  fseqen  9714  dfac8clem  9719  alephsson  9787  alephfp  9795  dfac4  9809  kmlem6  9842  kmlem8  9844  kmlem9  9845  infpssr  9995  fin1a2lem12  10098  axcc4  10126  axcc4dom  10128  ac6s2  10173  zornn0g  10192  cardidg  10235  unsnen  10240  pwcfsdom  10270  cfpwsdom  10271  gchpwdom  10357  r1tskina  10469  intgru  10501  indpi  10594  nqereu  10616  supsrlem  10798  letrii  11030  dfnn3  11917  zaddcl  12290  nn0ind  12345  fnn0ind  12349  ublbneg  12602  nn01to3  12610  infmrp1  13007  fz0  13200  fzo1fzo0n0  13366  elfzom1elp1fzo  13382  fzo0end  13407  elfznelfzo  13420  fzind2  13433  injresinjlem  13435  fleqceilz  13502  nnsinds  13636  nn0sinds  13637  faclbnd4lem1  13935  hashinf  13977  hasheqf1oi  13994  hashgt0elex  14044  hashgt23el  14067  hashfacen  14094  hashfacenOLD  14095  hash2prde  14112  hash2sspr  14130  fun2dmnop0  14136  iswrddm0  14169  swrdnnn0nd  14297  swrdnd0  14298  swrdlsw  14308  pfxn0  14327  pfxnd0  14329  swrdswrdlem  14345  pfxccatin12lem3  14373  pfxccat3  14375  pfxccat3a  14379  swrdccat3blem  14380  cshwsublen  14437  cshwidxmod  14444  repswcshw  14453  cshw1  14463  trclun  14653  dmtrclfv  14657  rediv  14770  imdiv  14777  sqrt0  14881  fsump1i  15409  modfsummods  15433  bpolydiflem  15692  bpoly3  15696  bpoly4  15697  cos1bnd  15824  sinltx  15826  rpnnen2lem1  15851  rpnnen2lem2  15852  rpnnen2lem12  15862  odd2np1  15978  opoe  16000  omoe  16001  opeo  16002  omeo  16003  gcdcllem1  16134  gcdaddmlem  16159  dfgcd2  16182  algfx  16213  lcmledvds  16232  lcmfunsnlem  16274  lcmfun  16278  coprmprod  16294  coprmproddvdslem  16295  odzval  16420  odzdvds  16424  prmreclem5  16549  mul4sq  16583  prmgaplem5  16684  prmgaplem6  16685  imasaddfnlem  17156  mreexexlem4d  17273  joindmss  18012  meetdmss  18026  gictr  18806  cntzval  18842  symg2bas  18915  odfval  19055  efgsfo  19260  efgrelexlemb  19271  dprddomcld  19519  dprdsubg  19542  dprd2da  19560  lssacs  20144  cnfldinv  20541  ocvval  20784  selvval  21238  dmatmul  21554  mdetfval1  21647  mndifsplit  21693  fvmptnn04if  21906  toprntopon  21982  opnnei  22179  ordtbas2  22250  ordtrest2lem  22262  lmmo  22439  fincmp  22452  bwth  22469  txbas  22626  ptcnplem  22680  tx2ndc  22710  hmphtr  22842  fbun  22899  filconn  22942  ptcmplem5  23115  cnextcn  23126  utoptop  23294  ucncn  23345  metust  23620  cfilucfil  23621  elcncf1di  23964  xrhmeo  24015  phtpycc  24060  copco  24087  pcohtpylem  24088  pcopt  24091  pcopt2  24092  ncvsi  24220  ovolval  24542  iunmbl2  24626  itg2splitlem  24818  cpnfval  25001  plyval  25259  fta1  25373  aaliou2b  25406  tayl0  25426  ulmdvlem3  25466  radcnvlem2  25478  dvradcnv  25485  reeff1o  25511  sincosq1lem  25559  sincosq2sgn  25561  sincosq4sgn  25563  sinq12ge0  25570  logrncl  25628  eflog  25637  cxpge0  25743  logb1  25824  atanf  25935  atanbnd  25981  igamf  26105  igamcl  26106  lgsne0  26388  mul2sq  26472  2sqreultblem  26501  pntibnd  26646  ostth  26692  mptelee  27166  axlowdimlem9  27221  axlowdimlem12  27224  axcontlem2  27236  axcontlem12  27246  structgrssvtx  27297  structgrssiedg  27298  lpvtx  27341  nbuhgr  27613  nbumgr  27617  nbuhgr2vtx1edgblem  27621  nbgr0vtxlem  27625  nbgr1vtx  27628  uvtx01vtx  27667  prcliscplgr  27684  cusgrsizeinds  27722  sizusglecusglem2  27732  uhgrvd00  27804  fusgrregdegfi  27839  rusgr1vtxlem  27857  wlkeq  27903  wlk1walk  27908  uspgr2wlkeq  27915  wlklenvclwlk  27924  wlklenvclwlkOLD  27925  wlkreslem  27939  wlkdlem2  27953  wlkdlem4  27955  spthonepeq  28021  clwlkclwwlkflem  28269  clwlkclwwlkfolem  28272  clwlkclwwlkf  28273  clwwisshclwws  28280  clwwlkneq0  28294  3wlkdlem6  28430  eupth2eucrct  28482  eupth2lem1  28483  eupth2lem3lem7  28499  frgr3vlem1  28538  frgr3vlem2  28539  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  numclwwlk5  28653  frgrreg  28659  frgrregord013  28660  friendshipgt3  28663  isgrpo  28760  vciOLD  28824  vcex  28841  nmogtmnf  29033  siilem1  29114  siii  29116  ajmoi  29121  bcsiALT  29442  hhcms  29466  ocval  29543  hsupval  29597  omlsilem  29665  h1de2bi  29817  h1de2ctlem  29818  hosubeq0i  30089  adjmo  30095  nmopgtmnf  30131  nlfnval  30144  nmcopex  30292  nmcfnex  30316  riesz4i  30326  riesz1  30328  riesz2  30329  opsqrlem1  30403  superpos  30617  hatomistici  30625  chpssati  30626  mdsymlem3  30668  3o1cs  30713  3o2cs  30714  3o3cs  30715  iunrnmptss  30806  brabgaf  30849  f1mptrn  30871  ffsrn  30966  fpwrelmap  30970  xnn0gt0  30994  hashxpe  31029  prmidl2  31518  mxidlnzrb  31546  fedgmul  31614  ordtrest2NEWlem  31774  qqhval2  31832  esumfsup  31938  esumcvg  31954  cntnevol  32096  ddemeas  32104  dya2icoseg2  32145  dya2iocnei  32149  eulerpartlems  32227  eulerpartlemgvv  32243  eulerpart  32249  cndprobprob  32305  ballotlemsdom  32378  ballotth  32404  sgn3da  32408  bnj945  32653  bnj1379  32710  bnj1459  32723  bnj557  32781  bnj571  32786  bnj849  32805  bnj964  32823  bnj978  32829  bnj1018g  32843  bnj1018  32844  bnj1020  32845  bnj1033  32849  bnj1175  32884  bnj1398  32914  bnj1417  32921  bnj1523  32951  nummin  32963  cusgr3cyclex  32998  txpconn  33094  satfv1  33225  satffun  33271  msubco  33393  mclsax  33431  setinds  33660  dfon2lem7  33671  dfon2lem8  33672  poseq  33729  soseq  33730  on2recsov  33754  nocvxminlem  33899  nocvxmin  33900  norec2ov  34041  pprodss4v  34113  fullfunfv  34176  altxpsspw  34206  funtransport  34260  fvtransport  34261  funray  34369  fvray  34370  funline  34371  fvline  34373  finminlem  34434  bisym1  34535  onsucconni  34553  onsucsuccmpi  34559  bj-currypara  34667  bj-alcomexcom  34789  axc11n11r  34792  bj-equsal2  34935  bj-xpima1snALT  35074  bj-bm1.3ii  35162  bj-opelidb1ALT  35264  mptsnunlem  35436  iooelexlt  35460  relowlpssretop  35462  rdgeqoa  35468  difunieq  35472  nlpineqsn  35506  fvineqsneq  35510  wl-lem-nexmo  35649  matunitlindflem1  35700  ptrecube  35704  poimirlem26  35730  poimirlem30  35734  poimir  35737  ismblfin  35745  itg2addnclem  35755  dvasin  35788  sdclem2  35827  totbndbnd  35874  ismgmOLD  35935  exidresid  35964  isrngo  35982  rngoablo2  35994  rngoueqz  36025  isdivrngo  36035  isdrngo1  36041  isdrngo2  36043  ispridl2  36123  relcnveq3  36383  elrelscnveq3  36536  ax12eq  36882  ax12el  36883  lkr0f  37035  hl2at  37346  dalemswapyz  37597  pclfinclN  37891  osumcllem11N  37907  pexmidlem8N  37918  ltrnnid  38077  aks4d1p8  40023  sn-00id  40305  mptfcl  40458  fphpd  40554  elmnc  40877  itgoval  40902  arearect  40962  reabsifpos  41131  clsk3nimkb  41539  grumnud  41793  nanorxor  41812  pm11.71  41904  iotavalsb  41940  sbiota1  41941  2uasbanh  42070  eel0TT  42213  eelT00  42214  eelTTT  42215  eelT11  42216  eelT12  42218  eelTT1  42219  eelT01  42220  eel0T1  42221  eelTT  42280  uunT1p1  42290  uun121  42292  uun121p1  42293  un2122  42299  uunTT1  42302  uunTT1p1  42303  uunTT1p2  42304  uunT11  42305  uunT11p1  42306  uunT11p2  42307  uunT12  42308  uunT12p1  42309  uunT12p2  42310  uunT12p3  42311  uunT12p4  42312  uunT12p5  42313  uun111  42314  3anidm12p2  42316  uun123  42317  3impdirp1  42325  undif3VD  42391  ax6e2ndeqVD  42418  2uasbanhVD  42420  ax6e2ndeqALT  42440  iunconnlem2  42444  sineq0ALT  42446  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem3  43434  stoweidlem17  43448  fourierdlem42  43580  fourierdlem48  43585  fourierdlem50  43587  fourierdlem51  43588  fourierdlem76  43613  fourierdlem83  43620  fourierdlem87  43624  hoidmvval0  44015  rexrsb  44479  2reu8i  44492  2reuimp  44494  afv0nbfvbi  44530  afvfv0bi  44531  afveu  44532  fnbrafvb  44533  afvres  44551  tz6.12-afv  44552  dmfcoafv  44554  afvco2  44555  aovprc  44567  aovrcl  44568  aovmpt4g  44580  afv2eu  44617  afv2res  44618  tz6.12-afv2  44619  tz6.12i-afv2  44622  afv2rnfveq  44641  fvmptrab  44671  fvmptrabdm  44672  fzopred  44702  2ffzoeq  44708  elsprel  44815  prproropf1o  44847  reupr  44862  lighneal  44951  odd2prm2  45058  even3prm2  45059  upgrwlkupwlk  45190  ovn0ssdmfun  45209  islinindfis  45678  rrx2linest  45976  line2ylem  45985  mofeu  46063  isthincd2  46207  setrec2fun  46284  elsetrecslem  46290  setrecsres  46293  secval  46335  cscval  46336  cotval  46337