Theorem sylbir 225

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3imtr3i  280  ex  450  3ori  1388  19.38  1766  19.35  1805  equsex  2292  nfeqf2  2297  sbi2  2393  mo2v  2477  2mo  2551  axie2  2597  necon1bi  2822  necon1i  2827  sbhypf  3253  vtocl2  3261  vtocl3  3262  reu6  3395  uneqin  3878  difin0ss  3946  inelcm  4032  falseral0  4081  difprsn1  4330  tppreqb  4336  n0snor2el  4364  unissint  4501  intminss  4503  iununi  4610  bm1.3ii  4784  eusv2nf  4864  reusv3i  4875  reuxfr2d  4891  moabex  4927  copsex2g  4958  opelopabt  4987  eqrelrel  5221  opeliunxp2  5260  opelrn  5357  issref  5509  ssxpb  5568  xpima  5576  xpimasn  5579  dmsn0el  5604  relcoi2  5663  elsnxp  5677  elsnxpOLD  5678  iotanul  5866  dffv2  6271  fnfvrnss  6390  fressnfv  6427  fconst5  6471  f1mpt  6518  isocnv3  6582  f1owe  6603  ovprc  6683  onminesb  6998  onminsb  6999  onintrab  7001  onnminsb  7004  onsucuni2  7034  tfindsg2  7061  zfrep6  7134  fo1stres  7192  fo2ndres  7193  bropopvvv  7255  bropfvvvv  7257  frxp  7287  opeliunxp2f  7336  mpt2xopoveqd  7347  reldmtpos  7360  wfrlem4  7418  wfrlem12  7426  wfrlem16  7430  wfr2  7434  tfrlem5  7476  tfrlem9  7481  tfr2  7494  rdgsuc  7520  oaordi  7626  oeordi  7667  omopthi  7737  fvmptmap  7894  mptelixpg  7945  ener  8002  enerOLD  8003  domtr  8009  snfi  8038  unen  8040  xpf1o  8122  mapen  8124  unxpdomlem3  8166  isinf  8173  frfi  8205  unblem1  8212  unfi  8227  fofinf1o  8241  fsuppun  8294  inf3lem2  8526  inf3lem5  8529  cantnfp1lem1  8575  cantnfp1lem3  8577  tcmin  8617  r1ordg  8641  r1ord  8643  rankr1ai  8661  r1val3  8701  bndrank  8704  unbndrank  8705  rankr1b  8727  rankxplim3  8744  tcrank  8747  xpnum  8777  cardmin2  8824  infxpenlem  8836  fseqen  8850  dfac8clem  8855  alephsson  8923  alephfp  8931  dfac4  8945  kmlem6  8977  kmlem8  8979  kmlem9  8980  infpssr  9130  fin1a2lem12  9233  axcc4  9261  axcc4dom  9263  ac6s2  9308  zornn0g  9327  cardidg  9370  unsnen  9375  pwcfsdom  9405  cfpwsdom  9406  gchpwdom  9492  r1tskina  9604  intgru  9636  indpi  9729  nqereu  9751  supsrlem  9932  letrii  10162  dfnn3  11034  zaddcl  11417  nn0ind  11472  fnn0ind  11476  ublbneg  11773  nn01to3  11781  infmrp1  12174  fz0  12356  fzo1fzo0n0  12518  elfzom1elp1fzo  12534  fzo0end  12560  elfznelfzo  12573  fzind2  12586  injresinjlem  12588  fleqceilz  12653  nnsinds  12787  nn0sinds  12788  faclbnd4lem1  13080  hashinf  13122  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashgt0elex  13189  hashfacen  13238  hash2prde  13252  hash2sspr  13270  fun2dmnop0  13276  swrdn0  13430  swrdlsw  13452  swrdswrdlem  13459  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat3blem  13495  cshwsublen  13542  cshwidxmod  13549  repswcshw  13558  cshw1  13568  trclun  13755  dmtrclfv  13759  rediv  13871  imdiv  13878  sqrt0  13982  fsump1i  14500  modfsummods  14525  bpolydiflem  14785  bpoly3  14789  bpoly4  14790  cos1bnd  14917  sinltx  14919  rpnnen2lem1  14943  rpnnen2lem2  14944  rpnnen2lem12  14954  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  gcdcllem1  15221  gcdaddmlem  15245  dfgcd2  15263  algfx  15293  lcmledvds  15312  lcmfunsnlem  15354  lcmfun  15358  coprmprod  15375  coprmproddvdslem  15376  prmn2uzge3OLD  15413  odzval  15496  odzdvds  15500  prmreclem5  15624  mul4sq  15658  prmgaplem5  15759  prmgaplem6  15760  imasaddfnlem  16188  mreexexlem4d  16307  joindmss  17007  meetdmss  17021  gictr  17717  cntzval  17754  symg2bas  17818  efgsfo  18152  efgrelexlemb  18163  dprddomcld  18400  dprdsubg  18423  dprd2da  18441  lssacs  18967  cnfldinv  19777  ocvval  20011  dmatmul  20303  mdetfval1  20396  mndifsplit  20442  fvmptnn04if  20654  opnnei  20924  ordtbas2  20995  ordtrest2lem  21007  lmmo  21184  fincmp  21196  bwth  21213  txbas  21370  ptcnplem  21424  tx2ndc  21454  hmphtr  21586  fbun  21644  filconn  21687  ptcmplem5  21860  cnextcn  21871  utoptop  22038  ucncn  22089  metust  22363  cfilucfil  22364  elcncf1di  22698  xrhmeo  22745  phtpycc  22790  copco  22818  pcohtpylem  22819  pcopt  22822  pcopt2  22823  ncvsi  22951  ovolval  23242  iunmbl2  23325  itg2splitlem  23515  cpnfval  23695  plyval  23949  fta1  24063  aaliou2b  24096  tayl0  24116  ulmdvlem3  24156  radcnvlem2  24168  dvradcnv  24175  reeff1o  24201  sincosq1lem  24249  sincosq2sgn  24251  sincosq4sgn  24253  sinq12ge0  24260  logrncl  24314  eflog  24323  cxpge0  24429  logb1  24507  atanf  24607  atanbnd  24653  igamf  24777  igamcl  24778  lgsne0  25060  mul2sq  25144  pntibnd  25282  ostth  25328  mptelee  25775  axlowdimlem9  25830  axlowdimlem12  25833  axcontlem2  25845  axcontlem12  25855  structgrssvtx  25913  structgrssiedg  25914  structgrssvtxOLD  25916  structgrssiedgOLD  25917  lpvtx  25963  nbuhgr  26239  nbumgr  26243  nbuhgr2vtx1edgblem  26247  nbgr0vtxlem  26251  nbgr1vtx  26254  uvtxa01vtx0  26297  cusgrsizeinds  26348  sizusglecusglem2  26358  uhgrvd00  26430  fusgrregdegfi  26465  rusgr1vtxlem  26483  wlkeq  26529  wlk1walk  26535  uspgr2wlkeq  26542  wlklenvclwlk  26551  wlkreslem  26566  wlkdlem2  26580  wlkdlem4  26582  spthonepeq  26648  clwwisshclwws  26928  3wlkdlem6  27025  eupth2eucrct  27077  eupth2lem1  27078  eupth2lem3lem7  27094  frgr3vlem1  27137  frgr3vlem2  27138  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  numclwwlk5  27246  frgrreg  27252  frgrregord013  27253  friendshipgt3  27256  isgrpo  27351  vciOLD  27416  vcex  27433  nmogtmnf  27625  siilem1  27706  siii  27708  ajmoi  27714  bcsiALT  28036  hhcms  28060  ocval  28139  hsupval  28193  omlsilem  28261  h1de2bi  28413  h1de2ctlem  28414  hosubeq0i  28685  adjmo  28691  nmopgtmnf  28727  nlfnval  28740  nmcopex  28888  nmcfnex  28912  riesz4i  28922  riesz1  28924  riesz2  28925  opsqrlem1  28999  superpos  29213  hatomistici  29221  chpssati  29222  mdsymlem3  29264  3o1cs  29309  3o2cs  29310  3o3cs  29311  spc2ed  29312  brabgaf  29420  f1mptrn  29435  ffsrn  29504  fpwrelmap  29508  ordtrest2NEWlem  29968  qqhval2  30026  esumfsup  30132  esumcvg  30148  cntnevol  30291  ddemeas  30299  dya2icoseg2  30340  dya2iocnei  30344  eulerpartlems  30422  eulerpartlemgvv  30438  eulerpart  30444  cndprobprob  30500  ballotlemsdom  30573  ballotth  30599  sgn3da  30603  bnj945  30844  bnj1379  30901  bnj1459  30913  bnj557  30971  bnj571  30976  bnj849  30995  bnj964  31013  bnj978  31019  bnj1018  31032  bnj1020  31033  bnj1033  31037  bnj1175  31072  bnj1398  31102  bnj1417  31109  bnj1523  31139  txpconn  31214  msubco  31428  mclsax  31466  setinds  31683  dfon2lem7  31694  dfon2lem8  31695  poseq  31750  soseq  31751  frrlem4  31783  frrlem11  31792  nocvxminlem  31893  nocvxmin  31894  pprodss4v  31991  fullfunfv  32054  altxpsspw  32084  funtransport  32138  fvtransport  32139  funray  32247  fvray  32248  funline  32249  fvline  32251  finminlem  32312  bisym1  32418  onsucconni  32436  onsucsuccmpi  32442  bj-alcomexcom  32670  axc11n11r  32673  bj-equsal2  32812  bj-xpima1snALT  32944  mptsnunlem  33185  iooelexlt  33210  relowlpssretop  33212  rdgeqoa  33218  wl-dveeq12  33311  wl-lem-nexmo  33349  matunitlindflem1  33405  ptrecube  33409  poimirlem26  33435  poimirlem30  33439  poimir  33442  ismblfin  33450  itg2addnclem  33461  dvasin  33496  sdclem2  33538  totbndbnd  33588  ismgmOLD  33649  exidresid  33678  isrngo  33696  rngoablo2  33708  rngoueqz  33739  isdivrngo  33749  isdrngo1  33755  isdrngo2  33757  ispridl2  33837  relcnveq3  34092  prtlem11  34151  ax12eq  34226  ax12el  34227  lkr0f  34381  hl2at  34691  dalemswapyz  34942  pclfinclN  35236  osumcllem11N  35252  pexmidlem8N  35263  ltrnnid  35422  mptfcl  37283  fphpd  37380  elmnc  37706  itgoval  37731  arearect  37801  clsk3nimkb  38338  nanorxor  38504  pm11.71  38597  iotavalsb  38634  sbiota1  38635  2uasbanh  38777  eel0TT  38929  eelT00  38930  eelTTT  38931  eelT11  38932  eelT12  38934  eelTT1  38935  eelT01  38936  eel0T1  38937  eelTT  38998  uunT1p1  39008  uun121  39010  uun121p1  39011  un2122  39017  uunTT1  39020  uunTT1p1  39021  uunTT1p2  39022  uunT11  39023  uunT11p1  39024  uunT11p2  39025  uunT12  39026  uunT12p1  39027  uunT12p2  39028  uunT12p3  39029  uunT12p4  39030  uunT12p5  39031  uun111  39032  3anidm12p2  39034  uun123  39035  3impdirp1  39043  undif3VD  39118  ax6e2ndeqVD  39145  2uasbanhVD  39147  ax6e2ndeqALT  39167  iunconnlem2  39171  sineq0ALT  39173  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem3  40220  stoweidlem17  40234  fourierdlem42  40366  fourierdlem48  40371  fourierdlem50  40373  fourierdlem51  40374  fourierdlem76  40399  fourierdlem83  40406  fourierdlem87  40410  hoidmvval0  40801  rexrsb  41169  raaan2  41175  afv0nbfvbi  41231  afvfv0bi  41232  afveu  41233  fnbrafvb  41234  afvres  41252  tz6.12-afv  41253  dmfcoafv  41255  afvco2  41256  aovprc  41268  aovrcl  41269  aovmpt4g  41281  fzopred  41332  2ffzoeq  41338  pfxccat3  41426  pfxccat3a  41429  lighneal  41528  odd2prm2  41627  even3prm2  41628  upgrwlkupwlk  41721  elsprel  41725  ovn0ssdmfun  41767  islinindfis  42238  setrec2fun  42439  elsetrecslem  42444  secval  42488  cscval  42489  cotval  42490