Theorem sylbir 235

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3i  291  ex  412  3expa  1118  3ori  1426  an42ds  1491  nanass  1511  19.38  1840  19.35  1878  19.8aw  2053  equsexv  2271  sbi2  2304  nfeqf2  2377  equsex  2418  dfmoeu  2531  2mo  2643  axie2  2698  necon1bi  2956  necon1i  2961  r19.35  3090  spc2ed  3551  reu6  3680  rabssrabd  4030  uneqin  4236  difin0ss  4320  inelcm  4412  rzal  4456  ralf0  4461  falseral0  4463  raaan2  4468  difprsn1  4749  tppreqb  4754  n0snor2el  4782  unissint  4920  intminss  4922  dfiun2g  4978  iununi  5045  triin  5212  bm1.3iiOLD  5238  eusv2nf  5331  reusv3i  5340  moabex  5397  opelopabt  5470  eqrelrel  5736  opeliunxp2  5777  opelrn  5882  ssxpb  6121  xpima  6129  xpimasn  6132  dmsn0el  6158  relcnvtr  6215  relcoi2  6224  elsnxp  6238  reuop  6240  iotanul  6461  f1imadifssran  6567  dffv2  6917  fnfvrnss  7054  fressnfv  7093  fconst5  7140  f1mpt  7195  isocnv3  7266  f1owe  7287  ovprc  7384  fvmpopr2d  7508  onminesb  7726  onminsb  7727  onintrab  7729  onnminsb  7732  ordsuci  7741  onsucuni2  7764  tfindsg2  7792  zfrep6  7887  fo1stres  7947  fo2ndres  7948  bropopvvv  8020  bropfvvvv  8022  frxp  8056  poseq  8088  soseq  8089  opeliunxp2f  8140  mpoxopoveqd  8151  reldmtpos  8164  frrlem4  8219  tfrlem5  8299  tfrlem9  8304  tfr2  8317  rdgsuc  8343  oaordi  8461  oeordi  8502  omopthi  8576  on2recsov  8583  fvmptmap  8805  mptelixpg  8859  ener  8923  domtr  8929  unen  8967  undom  8978  dom0  9018  xpf1o  9052  mapen  9054  pssnn  9078  unfi  9080  ssfi  9082  ensymfib  9093  entrfil  9094  enfii  9095  domtrfil  9101  unxpdomlem3  9142  isinf  9149  frfi  9169  unblem1  9176  fofinf1o  9216  fsuppun  9271  elirrv  9483  inf3lem2  9519  inf3lem5  9522  cantnfp1lem1  9568  cantnfp1lem3  9570  tcmin  9629  setinds  9639  frr2  9653  r1ordg  9671  r1ord  9673  rankr1ai  9691  r1val3  9731  bndrank  9734  unbndrank  9735  rankr1b  9757  rankxplim3  9774  tcrank  9777  xpnum  9844  cardmin2  9892  infxpenlem  9904  fseqen  9918  dfac8clem  9923  alephsson  9991  alephfp  9999  dfac4  10013  kmlem6  10047  kmlem8  10049  kmlem9  10050  cflem  10136  infpssr  10199  fin1a2lem12  10302  axcc4  10330  axcc4dom  10332  ac6s2  10377  zornn0g  10396  cardidg  10439  unsnen  10444  pwcfsdom  10474  cfpwsdom  10475  gchpwdom  10561  r1tskina  10673  intgru  10705  indpi  10798  nqereu  10820  supsrlem  11002  letrii  11238  dfnn3  12139  zaddcl  12512  nn0ind  12568  fnn0ind  12572  ublbneg  12831  nn01to3  12839  infmrp1  13244  fz0  13439  fzo1fzo0n0  13615  elfzom1elp1fzo  13632  fzo0end  13658  elfznelfzo  13673  fzind2  13688  injresinjlem  13690  fleqceilz  13758  nnsinds  13895  nn0sinds  13896  faclbnd4lem1  14200  hashinf  14242  hasheqf1oi  14258  hashgt0elex  14308  hashgt23el  14331  hashfacen  14361  hash2prde  14377  hash2sspr  14396  fun2dmnop0  14411  iswrddm0  14445  swrdnnn0nd  14564  swrdnd0  14565  swrdlsw  14575  pfxn0  14594  pfxnd0  14596  swrdswrdlem  14611  pfxccatin12lem3  14639  pfxccat3  14641  pfxccat3a  14645  swrdccat3blem  14646  cshwsublen  14703  cshwidxmod  14710  repswcshw  14719  cshw1  14729  trclun  14921  dmtrclfv  14925  rediv  15038  imdiv  15045  fsump1i  15676  modfsummods  15700  bpolydiflem  15961  bpoly3  15965  bpoly4  15966  cos1bnd  16096  sinltx  16098  rpnnen2lem1  16123  rpnnen2lem2  16124  rpnnen2lem12  16134  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  gcdcllem1  16410  gcdaddmlem  16435  dfgcd2  16457  algfx  16491  lcmledvds  16510  lcmfunsnlem  16552  lcmfun  16556  coprmprod  16572  coprmproddvdslem  16573  odzval  16703  odzdvds  16707  prmreclem5  16832  mul4sq  16866  prmgaplem5  16967  prmgaplem6  16968  imasaddfnlem  17432  mreexexlem4d  17553  joindmss  18283  meetdmss  18297  gictr  19188  cntzval  19233  symg2bas  19305  odfval  19444  efgsfo  19651  efgrelexlemb  19662  dprddomcld  19915  dprdsubg  19938  dprd2da  19956  lssacs  20900  cnfldinv  21339  pzriprnglem7  21424  ocvval  21604  selvval  22050  dmatmul  22412  mdetfval1  22505  mndifsplit  22551  fvmptnn04if  22764  toprntopon  22840  opnnei  23035  ordtbas2  23106  ordtrest2lem  23118  lmmo  23295  fincmp  23308  bwth  23325  txbas  23482  ptcnplem  23536  tx2ndc  23566  hmphtr  23698  fbun  23755  filconn  23798  ptcmplem5  23971  cnextcn  23982  utoptop  24149  ucncn  24199  metust  24473  cfilucfil  24474  elcncf1di  24815  xrhmeo  24871  phtpycc  24917  copco  24945  pcohtpylem  24946  pcopt  24949  pcopt2  24950  ncvsi  25078  ovolval  25401  iunmbl2  25485  itg2splitlem  25676  cpnfval  25861  plyval  26125  fta1  26243  aaliou2b  26276  tayl0  26296  ulmdvlem3  26338  radcnvlem2  26350  dvradcnv  26357  reeff1o  26384  sincosq1lem  26433  sincosq2sgn  26435  sincosq4sgn  26437  sinq12ge0  26444  logrncl  26503  eflog  26512  cxpge0  26619  logb1  26706  atanf  26817  atanbnd  26863  igamf  26988  igamcl  26989  lgsne0  27273  mul2sq  27357  2sqreultblem  27386  pntibnd  27531  ostth  27577  nobdaymin  27716  nocvxminlem  27717  cutlt  27876  norec2ov  27900  addsuniflem  27944  mulsuniflem  28088  zmulscld  28321  zseo  28345  zs12addscl  28387  mptelee  28873  axlowdimlem9  28928  axlowdimlem12  28931  axcontlem2  28943  axcontlem12  28953  structgrssvtx  29002  structgrssiedg  29003  lpvtx  29046  nbuhgr  29321  nbumgr  29325  nbuhgr2vtx1edgblem  29329  nbgr0edglem  29334  nbgr1vtx  29336  uvtx01vtx  29375  prcliscplgr  29392  cusgrsizeinds  29431  sizusglecusglem2  29441  uhgrvd00  29513  fusgrregdegfi  29548  rusgr1vtxlem  29566  wlkeq  29612  wlk1walk  29617  uspgr2wlkeq  29624  wlklenvclwlk  29632  wlkreslem  29646  wlkdlem2  29660  wlkdlem4  29662  spthonepeq  29730  cyclnumvtx  29778  clwlkclwwlkflem  29984  clwlkclwwlkfolem  29987  clwlkclwwlkf  29988  clwwisshclwws  29995  clwwlkneq0  30009  3wlkdlem6  30145  eupth2eucrct  30197  eupth2lem1  30198  eupth2lem3lem7  30214  frgr3vlem1  30253  frgr3vlem2  30254  frgrncvvdeqlem8  30286  frgrncvvdeqlem9  30287  numclwwlk5  30368  frgrreg  30374  frgrregord013  30375  friendshipgt3  30378  isgrpo  30477  vciOLD  30541  vcex  30558  nmogtmnf  30750  siilem1  30831  siii  30833  ajmoi  30838  bcsiALT  31159  hhcms  31183  ocval  31260  hsupval  31314  omlsilem  31382  h1de2bi  31534  h1de2ctlem  31535  hosubeq0i  31806  adjmo  31812  nmopgtmnf  31848  nlfnval  31861  nmcopex  32009  nmcfnex  32033  riesz4i  32043  riesz1  32045  riesz2  32046  opsqrlem1  32120  superpos  32334  hatomistici  32342  chpssati  32343  mdsymlem3  32385  3o1cs  32440  3o2cs  32441  3o3cs  32442  iunrnmptss  32545  brabgaf  32589  f1mptrn  32617  ffsrn  32711  fpwrelmap  32716  xnn0gt0  32752  hashxpe  32789  sgn3da  32817  elrgspnlem4  33212  prmidl2  33406  mxidlnzrb  33445  evl1deg2  33540  evl1deg3  33541  fedgmul  33644  cos9thpiminplylem2  33796  ordtrest2NEWlem  33935  qqhval2  33995  esumfsup  34083  esumcvg  34099  cntnevol  34241  ddemeas  34249  dya2icoseg2  34291  dya2iocnei  34295  eulerpartlems  34373  eulerpartlemgvv  34389  eulerpart  34395  cndprobprob  34451  ballotlemsdom  34525  ballotth  34551  bnj945  34785  bnj1379  34842  bnj1459  34855  bnj557  34913  bnj571  34918  bnj849  34937  bnj964  34955  bnj978  34961  bnj1018g  34975  bnj1018  34976  bnj1020  34977  bnj1033  34981  bnj1175  35016  bnj1398  35046  bnj1417  35053  bnj1523  35083  nummin  35104  r1omhf  35117  fineqvnttrclselem1  35141  onvf1odlem4  35150  onvf1od  35151  cusgr3cyclex  35180  txpconn  35276  satfv1  35407  satffun  35453  msubco  35575  mclsax  35613  dfon2lem7  35831  dfon2lem8  35832  pprodss4v  35926  fullfunfv  35991  altxpsspw  36021  funtransport  36075  fvtransport  36076  funray  36184  fvray  36185  funline  36186  fvline  36188  finminlem  36362  bisym1  36463  onsucconni  36481  onsucsuccmpi  36487  weiunse  36512  bj-currypara  36604  axc11n11r  36727  bj-equsal2  36869  bj-xpima1snALT  37001  bj-unexg  37082  bj-bm1.3ii  37108  bj-opelidb1ALT  37210  mptsnunlem  37382  iooelexlt  37406  relowlpssretop  37408  rdgeqoa  37414  difunieq  37418  nlpineqsn  37452  fvineqsneq  37456  wl-ax12v2cl  37550  wl-lem-nexmo  37611  matunitlindflem1  37666  ptrecube  37670  poimirlem26  37696  poimirlem30  37700  poimir  37703  ismblfin  37711  itg2addnclem  37721  dvasin  37754  sdclem2  37792  totbndbnd  37839  ismgmOLD  37900  exidresid  37929  isrngo  37947  rngoablo2  37959  rngoueqz  37990  isdivrngo  38000  isdrngo1  38006  isdrngo2  38008  ispridl2  38088  relcnveq3  38369  elrelscnveq3  38649  dmqsblocks  38961  ax12eq  39050  ax12el  39051  lkr0f  39203  hl2at  39514  dalemswapyz  39765  pclfinclN  40059  osumcllem11N  40075  pexmidlem8N  40086  ltrnnid  40245  aks4d1p8  42190  redvmptabs  42463  sn-00id  42504  rictr  42623  eu6w  42779  mptfcl  42823  fphpd  42919  elmnc  43239  itgoval  43264  arearect  43318  reabsifpos  43737  clsk3nimkb  44143  grumnud  44389  nanorxor  44408  pm11.71  44500  iotavalsb  44536  sbiota1  44537  2uasbanh  44664  eel0TT  44806  eelT00  44807  eelTTT  44808  eelT11  44809  eelT12  44811  eelTT1  44812  eelT01  44813  eel0T1  44814  eelTT  44873  uunT1p1  44883  uun121  44885  uun121p1  44886  un2122  44892  uunTT1  44895  uunTT1p1  44896  uunTT1p2  44897  uunT11  44898  uunT11p1  44899  uunT11p2  44900  uunT12  44901  uunT12p1  44902  uunT12p2  44903  uunT12p3  44904  uunT12p4  44905  uunT12p5  44906  uun111  44907  3anidm12p2  44909  uun123  44910  3impdirp1  44918  undif3VD  44984  ax6e2ndeqVD  45011  2uasbanhVD  45013  ax6e2ndeqALT  45033  iunconnlem2  45037  sineq0ALT  45039  modelaxreplem1  45081  permaxrep  45109  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  stoweidlem3  46111  stoweidlem17  46125  fourierdlem42  46257  fourierdlem48  46262  fourierdlem50  46264  fourierdlem51  46265  fourierdlem76  46290  fourierdlem83  46297  fourierdlem87  46301  hoidmvval0  46695  evenwodadd  46995  rexrsb  47210  2reu8i  47223  2reuimp  47225  afv0nbfvbi  47261  afvfv0bi  47262  afveu  47263  fnbrafvb  47264  afvres  47282  tz6.12-afv  47283  dmfcoafv  47285  afvco2  47286  aovprc  47298  aovrcl  47299  aovmpt4g  47311  afv2eu  47348  afv2res  47349  tz6.12-afv2  47350  tz6.12i-afv2  47353  afv2rnfveq  47372  fvmptrab  47402  fvmptrabdm  47403  fzopred  47432  2ffzoeq  47437  elsprel  47585  prproropf1o  47617  reupr  47632  lighneal  47721  odd2prm2  47828  even3prm2  47829  grictr  48033  grlimgrtrilem2  48112  usgrexmpl12ngric  48148  gpgprismgr4cycllem8  48212  gpgprismgr4cycllem11  48215  pgnbgreunbgrlem2lem1  48224  upgrwlkupwlk  48250  ovn0ssdmfun  48269  islinindfis  48560  rrx2linest  48853  line2ylem  48862  mofeu  48958  homf0  49120  uobffth  49329  uobeqw  49330  initopropd  49354  termopropd  49355  zeroopropd  49356  fucofvalne  49436  isthincd2  49548  lanrcl  49732  ranrcl  49733  setrec2fun  49803  elsetrecslem  49810  setrecsres  49813  secval  49858  cscval  49859  cotval  49860