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  291  ex  413  3expa  1117  3ori  1423  nanass  1505  19.38  1842  19.35  1881  19.8aw  2054  equsexv  2261  sbi2  2300  nfeqf2  2378  equsex  2419  dfmoeu  2537  2mo  2651  axie2  2705  necon1bi  2973  necon1i  2978  r19.35  3272  sbhypf  3492  spc2ed  3541  reu6  3662  rabssrabd  4017  uneqin  4213  difin0ss  4303  inelcm  4399  rzal  4440  ralf0  4445  falseral0  4451  raaan2  4456  difprsn1  4734  tppreqb  4739  n0snor2el  4765  unissint  4904  intminss  4906  dfiun2g  4961  iununi  5029  triin  5207  bm1.3ii  5227  eusv2nf  5319  reusv3i  5328  moabex  5375  copsex2gOLD  5409  opelopabt  5446  eqrelrel  5709  opeliunxp2  5750  opelrn  5855  ssxpb  6082  xpima  6090  xpimasn  6093  dmsn0el  6119  relcnvtr  6175  relcoi2  6184  elsnxp  6198  reuop  6200  iotanul  6415  dffv2  6872  fnfvrnss  7003  fressnfv  7041  fconst5  7090  f1mpt  7143  isocnv3  7212  f1owe  7233  ovprc  7322  fvmpopr2d  7443  onminesb  7652  onminsb  7653  onintrab  7655  onnminsb  7658  onsucuni2  7690  tfindsg2  7717  zfrep6  7806  fo1stres  7866  fo2ndres  7867  bropopvvv  7939  bropfvvvv  7941  frxp  7976  opeliunxp2f  8035  mpoxopoveqd  8046  reldmtpos  8059  frrlem4  8114  wfrlem4OLD  8152  wfrlem12OLD  8160  wfrlem16OLD  8164  wfr2OLD  8168  tfrlem5  8220  tfrlem9  8225  tfr2  8238  rdgsuc  8264  oaordi  8386  oeordi  8427  omopthi  8500  fvmptmap  8678  mptelixpg  8732  ener  8796  domtr  8802  snfi  8843  unen  8845  undom  8855  dom0  8898  xpf1o  8935  mapen  8937  rexdif1en  8953  dif1en  8954  pssnn  8960  unfi  8964  ssfi  8965  ensymfib  8979  entrfil  8980  enfii  8981  domtrfil  8987  unxpdomlem3  9038  isinf  9045  frfi  9068  unblem1  9075  unfiOLD  9090  fofinf1o  9103  fsuppun  9156  inf3lem2  9396  inf3lem5  9399  cantnfp1lem1  9445  cantnfp1lem3  9447  tcmin  9508  frr2  9527  r1ordg  9545  r1ord  9547  rankr1ai  9565  r1val3  9605  bndrank  9608  unbndrank  9609  rankr1b  9631  rankxplim3  9648  tcrank  9651  xpnum  9718  cardmin2  9766  infxpenlem  9778  fseqen  9792  dfac8clem  9797  alephsson  9865  alephfp  9873  dfac4  9887  kmlem6  9920  kmlem8  9922  kmlem9  9923  infpssr  10073  fin1a2lem12  10176  axcc4  10204  axcc4dom  10206  ac6s2  10251  zornn0g  10270  cardidg  10313  unsnen  10318  pwcfsdom  10348  cfpwsdom  10349  gchpwdom  10435  r1tskina  10547  intgru  10579  indpi  10672  nqereu  10694  supsrlem  10876  letrii  11109  dfnn3  11996  zaddcl  12369  nn0ind  12424  fnn0ind  12428  ublbneg  12682  nn01to3  12690  infmrp1  13087  fz0  13280  fzo1fzo0n0  13447  elfzom1elp1fzo  13463  fzo0end  13488  elfznelfzo  13501  fzind2  13514  injresinjlem  13516  fleqceilz  13583  nnsinds  13717  nn0sinds  13718  faclbnd4lem1  14016  hashinf  14058  hasheqf1oi  14075  hashgt0elex  14125  hashgt23el  14148  hashfacen  14175  hashfacenOLD  14176  hash2prde  14193  hash2sspr  14211  fun2dmnop0  14217  iswrddm0  14250  swrdnnn0nd  14378  swrdnd0  14379  swrdlsw  14389  pfxn0  14408  pfxnd0  14410  swrdswrdlem  14426  pfxccatin12lem3  14454  pfxccat3  14456  pfxccat3a  14460  swrdccat3blem  14461  cshwsublen  14518  cshwidxmod  14525  repswcshw  14534  cshw1  14544  trclun  14734  dmtrclfv  14738  rediv  14851  imdiv  14858  sqrt0  14962  fsump1i  15490  modfsummods  15514  bpolydiflem  15773  bpoly3  15777  bpoly4  15778  cos1bnd  15905  sinltx  15907  rpnnen2lem1  15932  rpnnen2lem2  15933  rpnnen2lem12  15943  odd2np1  16059  opoe  16081  omoe  16082  opeo  16083  omeo  16084  gcdcllem1  16215  gcdaddmlem  16240  dfgcd2  16263  algfx  16294  lcmledvds  16313  lcmfunsnlem  16355  lcmfun  16359  coprmprod  16375  coprmproddvdslem  16376  odzval  16501  odzdvds  16505  prmreclem5  16630  mul4sq  16664  prmgaplem5  16765  prmgaplem6  16766  imasaddfnlem  17248  mreexexlem4d  17365  joindmss  18106  meetdmss  18120  gictr  18900  cntzval  18936  symg2bas  19009  odfval  19149  efgsfo  19354  efgrelexlemb  19365  dprddomcld  19613  dprdsubg  19636  dprd2da  19654  lssacs  20238  cnfldinv  20638  ocvval  20881  selvval  21337  dmatmul  21655  mdetfval1  21748  mndifsplit  21794  fvmptnn04if  22007  toprntopon  22083  opnnei  22280  ordtbas2  22351  ordtrest2lem  22363  lmmo  22540  fincmp  22553  bwth  22570  txbas  22727  ptcnplem  22781  tx2ndc  22811  hmphtr  22943  fbun  23000  filconn  23043  ptcmplem5  23216  cnextcn  23227  utoptop  23395  ucncn  23446  metust  23723  cfilucfil  23724  elcncf1di  24067  xrhmeo  24118  phtpycc  24163  copco  24190  pcohtpylem  24191  pcopt  24194  pcopt2  24195  ncvsi  24324  ovolval  24646  iunmbl2  24730  itg2splitlem  24922  cpnfval  25105  plyval  25363  fta1  25477  aaliou2b  25510  tayl0  25530  ulmdvlem3  25570  radcnvlem2  25582  dvradcnv  25589  reeff1o  25615  sincosq1lem  25663  sincosq2sgn  25665  sincosq4sgn  25667  sinq12ge0  25674  logrncl  25732  eflog  25741  cxpge0  25847  logb1  25928  atanf  26039  atanbnd  26085  igamf  26209  igamcl  26210  lgsne0  26492  mul2sq  26576  2sqreultblem  26605  pntibnd  26750  ostth  26796  mptelee  27272  axlowdimlem9  27327  axlowdimlem12  27330  axcontlem2  27342  axcontlem12  27352  structgrssvtx  27403  structgrssiedg  27404  lpvtx  27447  nbuhgr  27719  nbumgr  27723  nbuhgr2vtx1edgblem  27727  nbgr0vtxlem  27731  nbgr1vtx  27734  uvtx01vtx  27773  prcliscplgr  27790  cusgrsizeinds  27828  sizusglecusglem2  27838  uhgrvd00  27910  fusgrregdegfi  27945  rusgr1vtxlem  27963  wlkeq  28010  wlk1walk  28015  uspgr2wlkeq  28022  wlklenvclwlk  28031  wlklenvclwlkOLD  28032  wlkreslem  28046  wlkdlem2  28060  wlkdlem4  28062  spthonepeq  28129  clwlkclwwlkflem  28377  clwlkclwwlkfolem  28380  clwlkclwwlkf  28381  clwwisshclwws  28388  clwwlkneq0  28402  3wlkdlem6  28538  eupth2eucrct  28590  eupth2lem1  28591  eupth2lem3lem7  28607  frgr3vlem1  28646  frgr3vlem2  28647  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  numclwwlk5  28761  frgrreg  28767  frgrregord013  28768  friendshipgt3  28771  isgrpo  28868  vciOLD  28932  vcex  28949  nmogtmnf  29141  siilem1  29222  siii  29224  ajmoi  29229  bcsiALT  29550  hhcms  29574  ocval  29651  hsupval  29705  omlsilem  29773  h1de2bi  29925  h1de2ctlem  29926  hosubeq0i  30197  adjmo  30203  nmopgtmnf  30239  nlfnval  30252  nmcopex  30400  nmcfnex  30424  riesz4i  30434  riesz1  30436  riesz2  30437  opsqrlem1  30511  superpos  30725  hatomistici  30733  chpssati  30734  mdsymlem3  30776  3o1cs  30821  3o2cs  30822  3o3cs  30823  iunrnmptss  30914  brabgaf  30957  f1mptrn  30979  ffsrn  31073  fpwrelmap  31077  xnn0gt0  31101  hashxpe  31136  prmidl2  31625  mxidlnzrb  31653  fedgmul  31721  ordtrest2NEWlem  31881  qqhval2  31941  esumfsup  32047  esumcvg  32063  cntnevol  32205  ddemeas  32213  dya2icoseg2  32254  dya2iocnei  32258  eulerpartlems  32336  eulerpartlemgvv  32352  eulerpart  32358  cndprobprob  32414  ballotlemsdom  32487  ballotth  32513  sgn3da  32517  bnj945  32762  bnj1379  32819  bnj1459  32832  bnj557  32890  bnj571  32895  bnj849  32914  bnj964  32932  bnj978  32938  bnj1018g  32952  bnj1018  32953  bnj1020  32954  bnj1033  32958  bnj1175  32993  bnj1398  33023  bnj1417  33030  bnj1523  33060  nummin  33072  cusgr3cyclex  33107  txpconn  33203  satfv1  33334  satffun  33380  msubco  33502  mclsax  33540  setinds  33763  dfon2lem7  33774  dfon2lem8  33775  poseq  33811  soseq  33812  on2recsov  33836  nocvxminlem  33981  nocvxmin  33982  norec2ov  34123  pprodss4v  34195  fullfunfv  34258  altxpsspw  34288  funtransport  34342  fvtransport  34343  funray  34451  fvray  34452  funline  34453  fvline  34455  finminlem  34516  bisym1  34617  onsucconni  34635  onsucsuccmpi  34641  bj-currypara  34749  bj-alcomexcom  34871  axc11n11r  34874  bj-equsal2  35017  bj-xpima1snALT  35156  bj-bm1.3ii  35244  bj-opelidb1ALT  35346  mptsnunlem  35518  iooelexlt  35542  relowlpssretop  35544  rdgeqoa  35550  difunieq  35554  nlpineqsn  35588  fvineqsneq  35592  wl-lem-nexmo  35731  matunitlindflem1  35782  ptrecube  35786  poimirlem26  35812  poimirlem30  35816  poimir  35819  ismblfin  35827  itg2addnclem  35837  dvasin  35870  sdclem2  35909  totbndbnd  35956  ismgmOLD  36017  exidresid  36046  isrngo  36064  rngoablo2  36076  rngoueqz  36107  isdivrngo  36117  isdrngo1  36123  isdrngo2  36125  ispridl2  36205  relcnveq3  36463  elrelscnveq3  36616  ax12eq  36962  ax12el  36963  lkr0f  37115  hl2at  37426  dalemswapyz  37677  pclfinclN  37971  osumcllem11N  37987  pexmidlem8N  37998  ltrnnid  38157  aks4d1p8  40102  sn-00id  40391  mptfcl  40549  fphpd  40645  elmnc  40968  itgoval  40993  arearect  41053  reabsifpos  41249  clsk3nimkb  41657  grumnud  41911  nanorxor  41930  pm11.71  42022  iotavalsb  42058  sbiota1  42059  2uasbanh  42188  eel0TT  42331  eelT00  42332  eelTTT  42333  eelT11  42334  eelT12  42336  eelTT1  42337  eelT01  42338  eel0T1  42339  eelTT  42398  uunT1p1  42408  uun121  42410  uun121p1  42411  un2122  42417  uunTT1  42420  uunTT1p1  42421  uunTT1p2  42422  uunT11  42423  uunT11p1  42424  uunT11p2  42425  uunT12  42426  uunT12p1  42427  uunT12p2  42428  uunT12p3  42429  uunT12p4  42430  uunT12p5  42431  uun111  42432  3anidm12p2  42434  uun123  42435  3impdirp1  42443  undif3VD  42509  ax6e2ndeqVD  42536  2uasbanhVD  42538  ax6e2ndeqALT  42558  iunconnlem2  42562  sineq0ALT  42564  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem3  43551  stoweidlem17  43565  fourierdlem42  43697  fourierdlem48  43702  fourierdlem50  43704  fourierdlem51  43705  fourierdlem76  43730  fourierdlem83  43737  fourierdlem87  43741  hoidmvval0  44132  rexrsb  44603  2reu8i  44616  2reuimp  44618  afv0nbfvbi  44654  afvfv0bi  44655  afveu  44656  fnbrafvb  44657  afvres  44675  tz6.12-afv  44676  dmfcoafv  44678  afvco2  44679  aovprc  44691  aovrcl  44692  aovmpt4g  44704  afv2eu  44741  afv2res  44742  tz6.12-afv2  44743  tz6.12i-afv2  44746  afv2rnfveq  44765  fvmptrab  44795  fvmptrabdm  44796  fzopred  44825  2ffzoeq  44831  elsprel  44938  prproropf1o  44970  reupr  44985  lighneal  45074  odd2prm2  45181  even3prm2  45182  upgrwlkupwlk  45313  ovn0ssdmfun  45332  islinindfis  45801  rrx2linest  46099  line2ylem  46108  mofeu  46186  isthincd2  46330  setrec2fun  46409  elsetrecslem  46415  setrecsres  46418  secval  46460  cscval  46461  cotval  46462