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  413  3expa  1118  3ori  1424  nanass  1508  19.38  1841  19.35  1880  19.8aw  2053  equsexv  2259  sbi2  2298  nfeqf2  2375  equsex  2416  dfmoeu  2529  2mo  2643  axie2  2697  necon1bi  2968  necon1i  2973  r19.35  3107  r19.35OLD  3108  sbhypfOLD  3509  spc2ed  3561  reu6  3687  rabssrabd  4046  uneqin  4243  difin0ss  4333  inelcm  4429  rzal  4471  ralf0  4476  falseral0  4482  raaan2  4487  difprsn1  4765  tppreqb  4770  n0snor2el  4796  unissint  4938  intminss  4940  dfiun2g  4995  iununi  5064  triin  5244  bm1.3ii  5264  eusv2nf  5355  reusv3i  5364  moabex  5421  copsex2gOLD  5456  opelopabt  5494  eqrelrel  5758  opeliunxp2  5799  opelrn  5903  ssxpb  6131  xpima  6139  xpimasn  6142  dmsn0el  6168  relcnvtr  6224  relcoi2  6234  elsnxp  6248  reuop  6250  iotanul  6479  dffv2  6941  fnfvrnss  7073  fressnfv  7111  fconst5  7160  f1mpt  7213  isocnv3  7282  f1owe  7303  ovprc  7400  fvmpopr2d  7521  onminesb  7733  onminsb  7734  onintrab  7736  onnminsb  7739  ordsuci  7748  onsucuni2  7774  tfindsg2  7803  zfrep6  7892  fo1stres  7952  fo2ndres  7953  bropopvvv  8027  bropfvvvv  8029  frxp  8063  poseq  8095  soseq  8096  opeliunxp2f  8146  mpoxopoveqd  8157  reldmtpos  8170  frrlem4  8225  wfrlem4OLD  8263  wfrlem12OLD  8271  wfrlem16OLD  8275  wfr2OLD  8279  tfrlem5  8331  tfrlem9  8336  tfr2  8349  rdgsuc  8375  oaordi  8498  oeordi  8539  omopthi  8612  on2recsov  8619  fvmptmap  8826  mptelixpg  8880  ener  8948  domtr  8954  snfi  8995  unen  8997  undom  9010  dom0  9053  xpf1o  9090  mapen  9092  rexdif1enOLD  9110  dif1enOLD  9113  pssnn  9119  unfi  9123  ssfi  9124  ensymfib  9138  entrfil  9139  enfii  9140  domtrfil  9146  unxpdomlem3  9203  isinf  9211  isinfOLD  9212  frfi  9239  unblem1  9246  unfiOLD  9264  fofinf1o  9278  fsuppun  9333  inf3lem2  9574  inf3lem5  9577  cantnfp1lem1  9623  cantnfp1lem3  9625  tcmin  9686  frr2  9705  r1ordg  9723  r1ord  9725  rankr1ai  9743  r1val3  9783  bndrank  9786  unbndrank  9787  rankr1b  9809  rankxplim3  9826  tcrank  9829  xpnum  9896  cardmin2  9944  infxpenlem  9958  fseqen  9972  dfac8clem  9977  alephsson  10045  alephfp  10053  dfac4  10067  kmlem6  10100  kmlem8  10102  kmlem9  10103  infpssr  10253  fin1a2lem12  10356  axcc4  10384  axcc4dom  10386  ac6s2  10431  zornn0g  10450  cardidg  10493  unsnen  10498  pwcfsdom  10528  cfpwsdom  10529  gchpwdom  10615  r1tskina  10727  intgru  10759  indpi  10852  nqereu  10874  supsrlem  11056  letrii  11289  dfnn3  12176  zaddcl  12552  nn0ind  12607  fnn0ind  12611  ublbneg  12867  nn01to3  12875  infmrp1  13273  fz0  13466  fzo1fzo0n0  13633  elfzom1elp1fzo  13649  fzo0end  13674  elfznelfzo  13687  fzind2  13700  injresinjlem  13702  fleqceilz  13769  nnsinds  13903  nn0sinds  13904  faclbnd4lem1  14203  hashinf  14245  hasheqf1oi  14261  hashgt0elex  14311  hashgt23el  14334  hashfacen  14363  hashfacenOLD  14364  hash2prde  14381  hash2sspr  14399  fun2dmnop0  14405  iswrddm0  14438  swrdnnn0nd  14556  swrdnd0  14557  swrdlsw  14567  pfxn0  14586  pfxnd0  14588  swrdswrdlem  14604  pfxccatin12lem3  14632  pfxccat3  14634  pfxccat3a  14638  swrdccat3blem  14639  cshwsublen  14696  cshwidxmod  14703  repswcshw  14712  cshw1  14722  trclun  14911  dmtrclfv  14915  rediv  15028  imdiv  15035  fsump1i  15665  modfsummods  15689  bpolydiflem  15948  bpoly3  15952  bpoly4  15953  cos1bnd  16080  sinltx  16082  rpnnen2lem1  16107  rpnnen2lem2  16108  rpnnen2lem12  16118  odd2np1  16234  opoe  16256  omoe  16257  opeo  16258  omeo  16259  gcdcllem1  16390  gcdaddmlem  16415  dfgcd2  16438  algfx  16467  lcmledvds  16486  lcmfunsnlem  16528  lcmfun  16532  coprmprod  16548  coprmproddvdslem  16549  odzval  16674  odzdvds  16678  prmreclem5  16803  mul4sq  16837  prmgaplem5  16938  prmgaplem6  16939  imasaddfnlem  17424  mreexexlem4d  17541  joindmss  18282  meetdmss  18296  gictr  19079  cntzval  19115  symg2bas  19188  odfval  19328  efgsfo  19535  efgrelexlemb  19546  dprddomcld  19794  dprdsubg  19817  dprd2da  19835  lssacs  20485  cnfldinv  20865  ocvval  21108  selvval  21565  dmatmul  21883  mdetfval1  21976  mndifsplit  22022  fvmptnn04if  22235  toprntopon  22311  opnnei  22508  ordtbas2  22579  ordtrest2lem  22591  lmmo  22768  fincmp  22781  bwth  22798  txbas  22955  ptcnplem  23009  tx2ndc  23039  hmphtr  23171  fbun  23228  filconn  23271  ptcmplem5  23444  cnextcn  23455  utoptop  23623  ucncn  23674  metust  23951  cfilucfil  23952  elcncf1di  24295  xrhmeo  24346  phtpycc  24391  copco  24418  pcohtpylem  24419  pcopt  24422  pcopt2  24423  ncvsi  24552  ovolval  24874  iunmbl2  24958  itg2splitlem  25150  cpnfval  25333  plyval  25591  fta1  25705  aaliou2b  25738  tayl0  25758  ulmdvlem3  25798  radcnvlem2  25810  dvradcnv  25817  reeff1o  25843  sincosq1lem  25891  sincosq2sgn  25893  sincosq4sgn  25895  sinq12ge0  25902  logrncl  25960  eflog  25969  cxpge0  26075  logb1  26156  atanf  26267  atanbnd  26313  igamf  26437  igamcl  26438  lgsne0  26720  mul2sq  26804  2sqreultblem  26833  pntibnd  26978  ostth  27024  nocvxminlem  27160  nocvxmin  27161  norec2ov  27312  addsunif  27353  mptelee  27907  axlowdimlem9  27962  axlowdimlem12  27965  axcontlem2  27977  axcontlem12  27987  structgrssvtx  28038  structgrssiedg  28039  lpvtx  28082  nbuhgr  28354  nbumgr  28358  nbuhgr2vtx1edgblem  28362  nbgr0vtxlem  28366  nbgr1vtx  28369  uvtx01vtx  28408  prcliscplgr  28425  cusgrsizeinds  28463  sizusglecusglem2  28473  uhgrvd00  28545  fusgrregdegfi  28580  rusgr1vtxlem  28598  wlkeq  28645  wlk1walk  28650  uspgr2wlkeq  28657  wlklenvclwlk  28666  wlkreslem  28680  wlkdlem2  28694  wlkdlem4  28696  spthonepeq  28763  clwlkclwwlkflem  29011  clwlkclwwlkfolem  29014  clwlkclwwlkf  29015  clwwisshclwws  29022  clwwlkneq0  29036  3wlkdlem6  29172  eupth2eucrct  29224  eupth2lem1  29225  eupth2lem3lem7  29241  frgr3vlem1  29280  frgr3vlem2  29281  frgrncvvdeqlem8  29313  frgrncvvdeqlem9  29314  numclwwlk5  29395  frgrreg  29401  frgrregord013  29402  friendshipgt3  29405  isgrpo  29502  vciOLD  29566  vcex  29583  nmogtmnf  29775  siilem1  29856  siii  29858  ajmoi  29863  bcsiALT  30184  hhcms  30208  ocval  30285  hsupval  30339  omlsilem  30407  h1de2bi  30559  h1de2ctlem  30560  hosubeq0i  30831  adjmo  30837  nmopgtmnf  30873  nlfnval  30886  nmcopex  31034  nmcfnex  31058  riesz4i  31068  riesz1  31070  riesz2  31071  opsqrlem1  31145  superpos  31359  hatomistici  31367  chpssati  31368  mdsymlem3  31410  3o1cs  31455  3o2cs  31456  3o3cs  31457  iunrnmptss  31551  brabgaf  31594  f1mptrn  31616  ffsrn  31714  fpwrelmap  31718  xnn0gt0  31742  hashxpe  31779  prmidl2  32289  mxidlnzrb  32317  fedgmul  32413  ordtrest2NEWlem  32592  qqhval2  32652  esumfsup  32758  esumcvg  32774  cntnevol  32916  ddemeas  32924  dya2icoseg2  32967  dya2iocnei  32971  eulerpartlems  33049  eulerpartlemgvv  33065  eulerpart  33071  cndprobprob  33127  ballotlemsdom  33200  ballotth  33226  sgn3da  33230  bnj945  33474  bnj1379  33531  bnj1459  33544  bnj557  33602  bnj571  33607  bnj849  33626  bnj964  33644  bnj978  33650  bnj1018g  33664  bnj1018  33665  bnj1020  33666  bnj1033  33670  bnj1175  33705  bnj1398  33735  bnj1417  33742  bnj1523  33772  nummin  33784  cusgr3cyclex  33817  txpconn  33913  satfv1  34044  satffun  34090  msubco  34212  mclsax  34250  setinds  34439  dfon2lem7  34450  dfon2lem8  34451  pprodss4v  34545  fullfunfv  34608  altxpsspw  34638  funtransport  34692  fvtransport  34693  funray  34801  fvray  34802  funline  34803  fvline  34805  finminlem  34866  bisym1  34967  onsucconni  34985  onsucsuccmpi  34991  bj-currypara  35099  axc11n11r  35224  bj-equsal2  35366  bj-xpima1snALT  35501  bj-unexg  35582  bj-bm1.3ii  35608  bj-opelidb1ALT  35710  mptsnunlem  35882  iooelexlt  35906  relowlpssretop  35908  rdgeqoa  35914  difunieq  35918  nlpineqsn  35952  fvineqsneq  35956  wl-lem-nexmo  36095  matunitlindflem1  36147  ptrecube  36151  poimirlem26  36177  poimirlem30  36181  poimir  36184  ismblfin  36192  itg2addnclem  36202  dvasin  36235  sdclem2  36274  totbndbnd  36321  ismgmOLD  36382  exidresid  36411  isrngo  36429  rngoablo2  36441  rngoueqz  36472  isdivrngo  36482  isdrngo1  36488  isdrngo2  36490  ispridl2  36570  relcnveq3  36855  elrelscnveq3  37026  ax12eq  37476  ax12el  37477  lkr0f  37629  hl2at  37941  dalemswapyz  38192  pclfinclN  38486  osumcllem11N  38502  pexmidlem8N  38513  ltrnnid  38672  aks4d1p8  40617  rictr  40769  sn-00id  40928  mptfcl  41101  fphpd  41197  elmnc  41521  itgoval  41546  arearect  41607  reabsifpos  42028  clsk3nimkb  42434  grumnud  42688  nanorxor  42707  pm11.71  42799  iotavalsb  42835  sbiota1  42836  2uasbanh  42965  eel0TT  43108  eelT00  43109  eelTTT  43110  eelT11  43111  eelT12  43113  eelTT1  43114  eelT01  43115  eel0T1  43116  eelTT  43175  uunT1p1  43185  uun121  43187  uun121p1  43188  un2122  43194  uunTT1  43197  uunTT1p1  43198  uunTT1p2  43199  uunT11  43200  uunT11p1  43201  uunT11p2  43202  uunT12  43203  uunT12p1  43204  uunT12p2  43205  uunT12p3  43206  uunT12p4  43207  uunT12p5  43208  uun111  43209  3anidm12p2  43211  uun123  43212  3impdirp1  43220  undif3VD  43286  ax6e2ndeqVD  43313  2uasbanhVD  43315  ax6e2ndeqALT  43335  iunconnlem2  43339  sineq0ALT  43341  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  stoweidlem3  44364  stoweidlem17  44378  fourierdlem42  44510  fourierdlem48  44515  fourierdlem50  44517  fourierdlem51  44518  fourierdlem76  44543  fourierdlem83  44550  fourierdlem87  44554  hoidmvval0  44948  rexrsb  45452  2reu8i  45465  2reuimp  45467  afv0nbfvbi  45503  afvfv0bi  45504  afveu  45505  fnbrafvb  45506  afvres  45524  tz6.12-afv  45525  dmfcoafv  45527  afvco2  45528  aovprc  45540  aovrcl  45541  aovmpt4g  45553  afv2eu  45590  afv2res  45591  tz6.12-afv2  45592  tz6.12i-afv2  45595  afv2rnfveq  45614  fvmptrab  45644  fvmptrabdm  45645  fzopred  45674  2ffzoeq  45680  elsprel  45787  prproropf1o  45819  reupr  45834  lighneal  45923  odd2prm2  46030  even3prm2  46031  upgrwlkupwlk  46162  ovn0ssdmfun  46181  islinindfis  46650  rrx2linest  46948  line2ylem  46957  mofeu  47034  isthincd2  47178  setrec2fun  47257  elsetrecslem  47264  setrecsres  47267  secval  47312  cscval  47313  cotval  47314