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  411  3expa  1116  3ori  1422  nanass  1506  19.38  1839  19.35  1878  19.8aw  2051  equsexv  2257  sbi2  2296  nfeqf2  2374  equsex  2415  dfmoeu  2528  2mo  2642  axie2  2696  necon1bi  2967  necon1i  2972  r19.35  3106  r19.35OLD  3107  sbhypfOLD  3538  spc2ed  3590  reu6  3721  rabssrabd  4080  uneqin  4277  difin0ss  4367  inelcm  4463  rzal  4507  ralf0  4512  falseral0  4518  raaan2  4523  difprsn1  4802  tppreqb  4807  n0snor2el  4833  unissint  4975  intminss  4977  dfiun2g  5032  iununi  5101  triin  5281  bm1.3ii  5301  eusv2nf  5392  reusv3i  5401  moabex  5458  copsex2gOLD  5493  opelopabt  5531  eqrelrel  5796  opeliunxp2  5837  opelrn  5941  ssxpb  6172  xpima  6180  xpimasn  6183  dmsn0el  6209  relcnvtr  6265  relcoi2  6275  elsnxp  6289  reuop  6291  iotanul  6520  dffv2  6985  fnfvrnss  7121  fressnfv  7159  fconst5  7208  f1mpt  7262  isocnv3  7331  f1owe  7352  ovprc  7449  fvmpopr2d  7571  onminesb  7783  onminsb  7784  onintrab  7786  onnminsb  7789  ordsuci  7798  onsucuni2  7824  tfindsg2  7853  zfrep6  7943  fo1stres  8003  fo2ndres  8004  bropopvvv  8078  bropfvvvv  8080  frxp  8114  poseq  8146  soseq  8147  opeliunxp2f  8197  mpoxopoveqd  8208  reldmtpos  8221  frrlem4  8276  wfrlem4OLD  8314  wfrlem12OLD  8322  wfrlem16OLD  8326  wfr2OLD  8330  tfrlem5  8382  tfrlem9  8387  tfr2  8400  rdgsuc  8426  oaordi  8548  oeordi  8589  omopthi  8662  on2recsov  8669  fvmptmap  8877  mptelixpg  8931  ener  8999  domtr  9005  snfi  9046  unen  9048  undom  9061  dom0  9104  xpf1o  9141  mapen  9143  rexdif1enOLD  9161  dif1enOLD  9164  pssnn  9170  unfi  9174  ssfi  9175  ensymfib  9189  entrfil  9190  enfii  9191  domtrfil  9197  unxpdomlem3  9254  isinf  9262  isinfOLD  9263  frfi  9290  unblem1  9297  unfiOLD  9315  fofinf1o  9329  fsuppun  9384  inf3lem2  9626  inf3lem5  9629  cantnfp1lem1  9675  cantnfp1lem3  9677  tcmin  9738  frr2  9757  r1ordg  9775  r1ord  9777  rankr1ai  9795  r1val3  9835  bndrank  9838  unbndrank  9839  rankr1b  9861  rankxplim3  9878  tcrank  9881  xpnum  9948  cardmin2  9996  infxpenlem  10010  fseqen  10024  dfac8clem  10029  alephsson  10097  alephfp  10105  dfac4  10119  kmlem6  10152  kmlem8  10154  kmlem9  10155  infpssr  10305  fin1a2lem12  10408  axcc4  10436  axcc4dom  10438  ac6s2  10483  zornn0g  10502  cardidg  10545  unsnen  10550  pwcfsdom  10580  cfpwsdom  10581  gchpwdom  10667  r1tskina  10779  intgru  10811  indpi  10904  nqereu  10926  supsrlem  11108  letrii  11343  dfnn3  12230  zaddcl  12606  nn0ind  12661  fnn0ind  12665  ublbneg  12921  nn01to3  12929  infmrp1  13327  fz0  13520  fzo1fzo0n0  13687  elfzom1elp1fzo  13703  fzo0end  13728  elfznelfzo  13741  fzind2  13754  injresinjlem  13756  fleqceilz  13823  nnsinds  13957  nn0sinds  13958  faclbnd4lem1  14257  hashinf  14299  hasheqf1oi  14315  hashgt0elex  14365  hashgt23el  14388  hashfacen  14417  hashfacenOLD  14418  hash2prde  14435  hash2sspr  14453  fun2dmnop0  14459  iswrddm0  14492  swrdnnn0nd  14610  swrdnd0  14611  swrdlsw  14621  pfxn0  14640  pfxnd0  14642  swrdswrdlem  14658  pfxccatin12lem3  14686  pfxccat3  14688  pfxccat3a  14692  swrdccat3blem  14693  cshwsublen  14750  cshwidxmod  14757  repswcshw  14766  cshw1  14776  trclun  14965  dmtrclfv  14969  rediv  15082  imdiv  15089  fsump1i  15719  modfsummods  15743  bpolydiflem  16002  bpoly3  16006  bpoly4  16007  cos1bnd  16134  sinltx  16136  rpnnen2lem1  16161  rpnnen2lem2  16162  rpnnen2lem12  16172  odd2np1  16288  opoe  16310  omoe  16311  opeo  16312  omeo  16313  gcdcllem1  16444  gcdaddmlem  16469  dfgcd2  16492  algfx  16521  lcmledvds  16540  lcmfunsnlem  16582  lcmfun  16586  coprmprod  16602  coprmproddvdslem  16603  odzval  16728  odzdvds  16732  prmreclem5  16857  mul4sq  16891  prmgaplem5  16992  prmgaplem6  16993  imasaddfnlem  17478  mreexexlem4d  17595  joindmss  18336  meetdmss  18350  gictr  19190  cntzval  19226  symg2bas  19301  odfval  19441  efgsfo  19648  efgrelexlemb  19659  dprddomcld  19912  dprdsubg  19935  dprd2da  19953  lssacs  20722  cnfldinv  21176  pzriprnglem7  21256  ocvval  21439  selvval  21900  dmatmul  22219  mdetfval1  22312  mndifsplit  22358  fvmptnn04if  22571  toprntopon  22647  opnnei  22844  ordtbas2  22915  ordtrest2lem  22927  lmmo  23104  fincmp  23117  bwth  23134  txbas  23291  ptcnplem  23345  tx2ndc  23375  hmphtr  23507  fbun  23564  filconn  23607  ptcmplem5  23780  cnextcn  23791  utoptop  23959  ucncn  24010  metust  24287  cfilucfil  24288  elcncf1di  24635  xrhmeo  24691  phtpycc  24737  copco  24765  pcohtpylem  24766  pcopt  24769  pcopt2  24770  ncvsi  24899  ovolval  25222  iunmbl2  25306  itg2splitlem  25498  cpnfval  25682  plyval  25942  fta1  26057  aaliou2b  26090  tayl0  26110  ulmdvlem3  26150  radcnvlem2  26162  dvradcnv  26169  reeff1o  26195  sincosq1lem  26243  sincosq2sgn  26245  sincosq4sgn  26247  sinq12ge0  26254  logrncl  26312  eflog  26321  cxpge0  26427  logb1  26510  atanf  26621  atanbnd  26667  igamf  26791  igamcl  26792  lgsne0  27074  mul2sq  27158  2sqreultblem  27187  pntibnd  27332  ostth  27378  nocvxminlem  27515  nocvxmin  27516  cutlt  27657  norec2ov  27679  addsuniflem  27723  mulsuniflem  27843  mptelee  28420  axlowdimlem9  28475  axlowdimlem12  28478  axcontlem2  28490  axcontlem12  28500  structgrssvtx  28551  structgrssiedg  28552  lpvtx  28595  nbuhgr  28867  nbumgr  28871  nbuhgr2vtx1edgblem  28875  nbgr0vtxlem  28879  nbgr1vtx  28882  uvtx01vtx  28921  prcliscplgr  28938  cusgrsizeinds  28976  sizusglecusglem2  28986  uhgrvd00  29058  fusgrregdegfi  29093  rusgr1vtxlem  29111  wlkeq  29158  wlk1walk  29163  uspgr2wlkeq  29170  wlklenvclwlk  29179  wlkreslem  29193  wlkdlem2  29207  wlkdlem4  29209  spthonepeq  29276  clwlkclwwlkflem  29524  clwlkclwwlkfolem  29527  clwlkclwwlkf  29528  clwwisshclwws  29535  clwwlkneq0  29549  3wlkdlem6  29685  eupth2eucrct  29737  eupth2lem1  29738  eupth2lem3lem7  29754  frgr3vlem1  29793  frgr3vlem2  29794  frgrncvvdeqlem8  29826  frgrncvvdeqlem9  29827  numclwwlk5  29908  frgrreg  29914  frgrregord013  29915  friendshipgt3  29918  isgrpo  30017  vciOLD  30081  vcex  30098  nmogtmnf  30290  siilem1  30371  siii  30373  ajmoi  30378  bcsiALT  30699  hhcms  30723  ocval  30800  hsupval  30854  omlsilem  30922  h1de2bi  31074  h1de2ctlem  31075  hosubeq0i  31346  adjmo  31352  nmopgtmnf  31388  nlfnval  31401  nmcopex  31549  nmcfnex  31573  riesz4i  31583  riesz1  31585  riesz2  31586  opsqrlem1  31660  superpos  31874  hatomistici  31882  chpssati  31883  mdsymlem3  31925  3o1cs  31970  3o2cs  31971  3o3cs  31972  iunrnmptss  32064  brabgaf  32104  f1mptrn  32126  ffsrn  32221  fpwrelmap  32225  xnn0gt0  32249  hashxpe  32286  prmidl2  32833  mxidlnzrb  32869  fedgmul  33004  ordtrest2NEWlem  33200  qqhval2  33260  esumfsup  33366  esumcvg  33382  cntnevol  33524  ddemeas  33532  dya2icoseg2  33575  dya2iocnei  33579  eulerpartlems  33657  eulerpartlemgvv  33673  eulerpart  33679  cndprobprob  33735  ballotlemsdom  33808  ballotth  33834  sgn3da  33838  bnj945  34082  bnj1379  34139  bnj1459  34152  bnj557  34210  bnj571  34215  bnj849  34234  bnj964  34252  bnj978  34258  bnj1018g  34272  bnj1018  34273  bnj1020  34274  bnj1033  34278  bnj1175  34313  bnj1398  34343  bnj1417  34350  bnj1523  34380  nummin  34392  cusgr3cyclex  34425  txpconn  34521  satfv1  34652  satffun  34698  msubco  34820  mclsax  34858  setinds  35054  dfon2lem7  35065  dfon2lem8  35066  pprodss4v  35160  fullfunfv  35223  altxpsspw  35253  funtransport  35307  fvtransport  35308  funray  35416  fvray  35417  funline  35418  fvline  35420  finminlem  35506  bisym1  35607  onsucconni  35625  onsucsuccmpi  35631  bj-currypara  35739  axc11n11r  35864  bj-equsal2  36006  bj-xpima1snALT  36141  bj-unexg  36222  bj-bm1.3ii  36248  bj-opelidb1ALT  36350  mptsnunlem  36522  iooelexlt  36546  relowlpssretop  36548  rdgeqoa  36554  difunieq  36558  nlpineqsn  36592  fvineqsneq  36596  wl-lem-nexmo  36735  matunitlindflem1  36787  ptrecube  36791  poimirlem26  36817  poimirlem30  36821  poimir  36824  ismblfin  36832  itg2addnclem  36842  dvasin  36875  sdclem2  36913  totbndbnd  36960  ismgmOLD  37021  exidresid  37050  isrngo  37068  rngoablo2  37080  rngoueqz  37111  isdivrngo  37121  isdrngo1  37127  isdrngo2  37129  ispridl2  37209  relcnveq3  37493  elrelscnveq3  37664  ax12eq  38114  ax12el  38115  lkr0f  38267  hl2at  38579  dalemswapyz  38830  pclfinclN  39124  osumcllem11N  39140  pexmidlem8N  39151  ltrnnid  39310  aks4d1p8  41258  rictr  41399  sn-00id  41576  mptfcl  41760  fphpd  41856  elmnc  42180  itgoval  42205  arearect  42266  reabsifpos  42687  clsk3nimkb  43093  grumnud  43347  nanorxor  43366  pm11.71  43458  iotavalsb  43494  sbiota1  43495  2uasbanh  43624  eel0TT  43767  eelT00  43768  eelTTT  43769  eelT11  43770  eelT12  43772  eelTT1  43773  eelT01  43774  eel0T1  43775  eelTT  43834  uunT1p1  43844  uun121  43846  uun121p1  43847  un2122  43853  uunTT1  43856  uunTT1p1  43857  uunTT1p2  43858  uunT11  43859  uunT11p1  43860  uunT11p2  43861  uunT12  43862  uunT12p1  43863  uunT12p2  43864  uunT12p3  43865  uunT12p4  43866  uunT12p5  43867  uun111  43868  3anidm12p2  43870  uun123  43871  3impdirp1  43879  undif3VD  43945  ax6e2ndeqVD  43972  2uasbanhVD  43974  ax6e2ndeqALT  43994  iunconnlem2  43998  sineq0ALT  44000  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem3  45017  stoweidlem17  45031  fourierdlem42  45163  fourierdlem48  45168  fourierdlem50  45170  fourierdlem51  45171  fourierdlem76  45196  fourierdlem83  45203  fourierdlem87  45207  hoidmvval0  45601  rexrsb  46106  2reu8i  46119  2reuimp  46121  afv0nbfvbi  46157  afvfv0bi  46158  afveu  46159  fnbrafvb  46160  afvres  46178  tz6.12-afv  46179  dmfcoafv  46181  afvco2  46182  aovprc  46194  aovrcl  46195  aovmpt4g  46207  afv2eu  46244  afv2res  46245  tz6.12-afv2  46246  tz6.12i-afv2  46249  afv2rnfveq  46268  fvmptrab  46298  fvmptrabdm  46299  fzopred  46328  2ffzoeq  46334  elsprel  46441  prproropf1o  46473  reupr  46488  lighneal  46577  odd2prm2  46684  even3prm2  46685  upgrwlkupwlk  46816  ovn0ssdmfun  46835  islinindfis  47217  rrx2linest  47515  line2ylem  47524  mofeu  47601  isthincd2  47745  setrec2fun  47824  elsetrecslem  47831  setrecsres  47834  secval  47879  cscval  47880  cotval  47881