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  1119  3ori  1427  an42ds  1492  nanass  1512  19.38  1841  19.35  1879  19.8aw  2054  equsexv  2276  sbi2  2309  nfeqf2  2382  equsex  2423  dfmoeu  2536  2mo  2649  axie2  2704  necon1bi  2961  necon1i  2966  r19.35  3096  spc2ed  3544  reu6  3673  rabssrabd  4024  uneqin  4230  difin0ss  4314  inelcm  4406  falseral0OLD  4456  raaan2  4463  difprsn1  4744  tppreqb  4749  n0snor2el  4777  unissint  4915  intminss  4917  dfiun2g  4973  iununi  5042  triin  5210  bm1.3iiOLD  5238  eusv2nf  5333  reusv3i  5342  axprglem  5374  axprg  5375  moabexOLD  5407  opelopabt  5481  eqrelrel  5747  opeliunxp2  5788  opelrn  5893  ssxpb  6133  xpima  6141  xpimasn  6144  dmsn0el  6170  relcnvtr  6227  relcoi2  6236  elsnxp  6250  reuop  6252  iotanul  6473  f1imadifssran  6579  dffv2  6930  fnfvrnss  7068  fressnfv  7108  fconst5  7155  f1mpt  7210  isocnv3  7281  f1owe  7302  ovprc  7399  fvmpopr2d  7523  onminesb  7741  onminsb  7742  onintrab  7744  onnminsb  7747  ordsuci  7756  onsucuni2  7779  tfindsg2  7807  zfrep6OLD  7902  fo1stres  7962  fo2ndres  7963  bropopvvv  8034  bropfvvvv  8036  frxp  8070  poseq  8102  soseq  8103  opeliunxp2f  8154  mpoxopoveqd  8165  reldmtpos  8178  frrlem4  8233  tfrlem5  8313  tfrlem9  8318  tfr2  8331  rdgsuc  8357  oaordi  8475  oeordi  8517  omopthi  8591  on2recsov  8598  fvmptmap  8823  mptelixpg  8877  ener  8942  domtr  8948  unen  8986  undom  8997  dom0  9037  xpf1o  9071  mapen  9073  pssnn  9097  unfi  9099  ssfi  9101  ensymfib  9112  entrfil  9113  enfii  9114  domtrfil  9120  unxpdomlem3  9162  isinf  9169  frfi  9189  unblem1  9196  fofinf1o  9236  fsuppun  9294  elirrv  9506  inf3lem2  9544  inf3lem5  9547  cantnfp1lem1  9593  cantnfp1lem3  9595  tcmin  9654  setinds  9664  frr2  9678  r1ordg  9696  r1ord  9698  rankr1ai  9716  r1val3  9756  bndrank  9759  unbndrank  9760  rankr1b  9782  rankxplim3  9799  tcrank  9802  xpnum  9869  cardmin2  9917  infxpenlem  9929  fseqen  9943  dfac8clem  9948  alephsson  10016  alephfp  10024  dfac4  10038  kmlem6  10072  kmlem8  10074  kmlem9  10075  cflem  10161  infpssr  10224  fin1a2lem12  10327  axcc4  10355  axcc4dom  10357  ac6s2  10402  zornn0g  10421  cardidg  10464  unsnen  10469  pwcfsdom  10500  cfpwsdom  10501  gchpwdom  10587  r1tskina  10699  intgru  10731  indpi  10824  nqereu  10846  supsrlem  11028  letrii  11265  dfnn3  12182  zaddcl  12561  nn0ind  12618  fnn0ind  12622  ublbneg  12877  nn01to3  12885  infmrp1  13291  fz0  13487  fzo1fzo0n0  13664  elfzom1elp1fzo  13681  fzo0end  13707  elfznelfzo  13722  fzind2  13737  injresinjlem  13739  fleqceilz  13807  nnsinds  13944  nn0sinds  13945  faclbnd4lem1  14249  hashinf  14291  hasheqf1oi  14307  hashgt0elex  14357  hashgt23el  14380  hashfacen  14410  hash2prde  14426  hash2sspr  14445  fun2dmnop0  14460  iswrddm0  14494  swrdnnn0nd  14613  swrdnd0  14614  swrdlsw  14624  pfxn0  14643  pfxnd0  14645  swrdswrdlem  14660  pfxccatin12lem3  14688  pfxccat3  14690  pfxccat3a  14694  swrdccat3blem  14695  cshwsublen  14752  cshwidxmod  14759  repswcshw  14768  cshw1  14778  trclun  14970  dmtrclfv  14974  rediv  15087  imdiv  15094  fsump1i  15725  modfsummods  15750  bpolydiflem  16013  bpoly3  16017  bpoly4  16018  cos1bnd  16148  sinltx  16150  rpnnen2lem1  16175  rpnnen2lem2  16176  rpnnen2lem12  16186  odd2np1  16304  opoe  16326  omoe  16327  opeo  16328  omeo  16329  gcdcllem1  16462  gcdaddmlem  16487  dfgcd2  16509  algfx  16543  lcmledvds  16562  lcmfunsnlem  16604  lcmfun  16608  coprmprod  16624  coprmproddvdslem  16625  odzval  16756  odzdvds  16760  prmreclem5  16885  mul4sq  16919  prmgaplem5  17020  prmgaplem6  17021  imasaddfnlem  17486  mreexexlem4d  17607  joindmss  18337  meetdmss  18351  gictr  19245  cntzval  19290  symg2bas  19362  odfval  19501  efgsfo  19708  efgrelexlemb  19719  dprddomcld  19972  dprdsubg  19995  dprd2da  20013  lssacs  20956  cnfldinv  21395  pzriprnglem7  21480  ocvval  21660  selvval  22114  dmatmul  22475  mdetfval1  22568  mndifsplit  22614  fvmptnn04if  22827  toprntopon  22903  opnnei  23098  ordtbas2  23169  ordtrest2lem  23181  lmmo  23358  fincmp  23371  bwth  23388  txbas  23545  ptcnplem  23599  tx2ndc  23629  hmphtr  23761  fbun  23818  filconn  23861  ptcmplem5  24034  cnextcn  24045  utoptop  24212  ucncn  24262  metust  24536  cfilucfil  24537  elcncf1di  24875  xrhmeo  24926  phtpycc  24971  copco  24998  pcohtpylem  24999  pcopt  25002  pcopt2  25003  ncvsi  25131  ovolval  25453  iunmbl2  25537  itg2splitlem  25728  cpnfval  25912  plyval  26171  fta1  26288  aaliou2b  26321  tayl0  26341  ulmdvlem3  26383  radcnvlem2  26395  dvradcnv  26402  reeff1o  26428  sincosq1lem  26477  sincosq2sgn  26479  sincosq4sgn  26481  sinq12ge0  26488  logrncl  26547  eflog  26556  cxpge0  26663  logb1  26749  atanf  26860  atanbnd  26906  igamf  27031  igamcl  27032  lgsne0  27315  mul2sq  27399  2sqreultblem  27428  pntibnd  27573  ostth  27619  nobdaymin  27762  nocvxminlem  27763  cutlt  27941  norec2ov  27966  addsuniflem  28010  mulsuniflem  28158  oldfib  28386  zmulscld  28406  zseo  28431  z12addscl  28486  mpteleeOLD  28981  axlowdimlem9  29036  axlowdimlem12  29039  axcontlem2  29051  axcontlem12  29061  structgrssvtx  29110  structgrssiedg  29111  lpvtx  29154  nbuhgr  29429  nbumgr  29433  nbuhgr2vtx1edgblem  29437  nbgr0edglem  29442  nbgr1vtx  29444  uvtx01vtx  29483  prcliscplgr  29500  cusgrsizeinds  29539  sizusglecusglem2  29549  uhgrvd00  29621  fusgrregdegfi  29656  rusgr1vtxlem  29674  wlkeq  29720  wlk1walk  29725  uspgr2wlkeq  29732  wlklenvclwlk  29740  wlkreslem  29754  wlkdlem2  29768  wlkdlem4  29770  spthonepeq  29838  cyclnumvtx  29886  clwlkclwwlkflem  30092  clwlkclwwlkfolem  30095  clwlkclwwlkf  30096  clwwisshclwws  30103  clwwlkneq0  30117  3wlkdlem6  30253  eupth2eucrct  30305  eupth2lem1  30306  eupth2lem3lem7  30322  frgr3vlem1  30361  frgr3vlem2  30362  frgrncvvdeqlem8  30394  frgrncvvdeqlem9  30395  numclwwlk5  30476  frgrreg  30482  frgrregord013  30483  friendshipgt3  30486  isgrpo  30586  vciOLD  30650  vcex  30667  nmogtmnf  30859  siilem1  30940  siii  30942  ajmoi  30947  bcsiALT  31268  hhcms  31292  ocval  31369  hsupval  31423  omlsilem  31491  h1de2bi  31643  h1de2ctlem  31644  hosubeq0i  31915  adjmo  31921  nmopgtmnf  31957  nlfnval  31970  nmcopex  32118  nmcfnex  32142  riesz4i  32152  riesz1  32154  riesz2  32155  opsqrlem1  32229  superpos  32443  hatomistici  32451  chpssati  32452  mdsymlem3  32494  3o1cs  32548  3o2cs  32549  3o3cs  32550  iunrnmptss  32653  brabgaf  32697  f1mptrn  32726  ffsrn  32819  xnn0gt0  32860  hashxpe  32898  sgn3da  32925  elrgspnlem4  33324  prmidl2  33519  mxidlnzrb  33558  evl1deg2  33655  evl1deg3  33656  fedgmul  33794  cos9thpiminplylem2  33946  ordtrest2NEWlem  34085  qqhval2  34145  esumfsup  34233  esumcvg  34249  cntnevol  34391  ddemeas  34399  dya2icoseg2  34441  dya2iocnei  34445  eulerpartlems  34523  eulerpartlemgvv  34539  eulerpart  34545  cndprobprob  34601  ballotlemsdom  34675  ballotth  34701  bnj945  34935  bnj1379  34991  bnj1459  35004  bnj557  35062  bnj571  35067  bnj849  35086  bnj964  35104  bnj978  35110  bnj1018g  35124  bnj1018  35125  bnj1020  35126  bnj1033  35130  bnj1175  35165  bnj1398  35195  bnj1417  35202  bnj1523  35232  nummin  35255  r1omhf  35268  axprALT2  35272  fineqvnttrclselem1  35284  onvf1odlem4  35307  onvf1od  35308  cusgr3cyclex  35337  txpconn  35433  satfv1  35564  satffun  35610  msubco  35732  mclsax  35770  dfon2lem7  35988  dfon2lem8  35989  pprodss4v  36083  fullfunfv  36148  altxpsspw  36178  funtransport  36232  fvtransport  36233  funray  36341  fvray  36342  funline  36343  fvline  36345  finminlem  36519  bisym1  36620  onsucconni  36638  onsucsuccmpi  36644  weiunse  36669  bj-currypara  36843  bj-cbvaw  36954  axc11n11r  36999  bj-equsal2  37151  bj-xpima1snALT  37283  bj-unexg  37364  bj-bm1.3ii  37390  bj-axseprep  37400  bj-axreprepsep  37401  bj-opelidb1ALT  37499  mptsnunlem  37671  iooelexlt  37695  relowlpssretop  37697  rdgeqoa  37703  difunieq  37707  nlpineqsn  37741  fvineqsneq  37745  wl-ax12v2cl  37839  wl-lem-nexmo  37909  matunitlindflem1  37954  ptrecube  37958  poimirlem26  37984  poimirlem30  37988  poimir  37991  ismblfin  37999  itg2addnclem  38009  dvasin  38042  sdclem2  38080  totbndbnd  38127  ismgmOLD  38188  exidresid  38217  isrngo  38235  rngoablo2  38247  rngoueqz  38278  isdivrngo  38288  isdrngo1  38294  isdrngo2  38296  ispridl2  38376  relcnveq3  38665  elrelscnveq3  38965  disjimeceqim  39142  dmqsblocks  39305  ax12eq  39404  ax12el  39405  lkr0f  39557  hl2at  39868  dalemswapyz  40119  pclfinclN  40413  osumcllem11N  40429  pexmidlem8N  40440  ltrnnid  40599  aks4d1p8  42543  redvmptabs  42809  sn-00id  42850  rictr  42982  eu6w  43126  mptfcl  43169  fphpd  43265  elmnc  43585  itgoval  43610  arearect  43664  reabsifpos  44082  clsk3nimkb  44488  grumnud  44734  nanorxor  44753  pm11.71  44845  iotavalsb  44881  sbiota1  44882  2uasbanh  45009  eel0TT  45151  eelT00  45152  eelTTT  45153  eelT11  45154  eelT12  45156  eelTT1  45157  eelT01  45158  eel0T1  45159  eelTT  45218  uunT1p1  45228  uun121  45230  uun121p1  45231  un2122  45237  uunTT1  45240  uunTT1p1  45241  uunTT1p2  45242  uunT11  45243  uunT11p1  45244  uunT11p2  45245  uunT12  45246  uunT12p1  45247  uunT12p2  45248  uunT12p3  45249  uunT12p4  45250  uunT12p5  45251  uun111  45252  3anidm12p2  45254  uun123  45255  3impdirp1  45263  undif3VD  45329  ax6e2ndeqVD  45356  2uasbanhVD  45358  ax6e2ndeqALT  45378  iunconnlem2  45382  sineq0ALT  45384  modelaxreplem1  45426  permaxrep  45454  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  stoweidlem3  46452  stoweidlem17  46466  fourierdlem42  46598  fourierdlem48  46603  fourierdlem50  46605  fourierdlem51  46606  fourierdlem76  46631  fourierdlem83  46638  fourierdlem87  46642  hoidmvval0  47036  evenwodadd  47336  rexrsb  47563  2reu8i  47576  2reuimp  47578  afv0nbfvbi  47614  afvfv0bi  47615  afveu  47616  fnbrafvb  47617  afvres  47635  tz6.12-afv  47636  dmfcoafv  47638  afvco2  47639  aovprc  47651  aovrcl  47652  aovmpt4g  47664  afv2eu  47701  afv2res  47702  tz6.12-afv2  47703  tz6.12i-afv2  47706  afv2rnfveq  47725  fvmptrab  47755  fvmptrabdm  47756  fzopred  47786  2ffzoeq  47791  muldvdsfacm1  47850  elsprel  47950  prproropf1o  47982  reupr  47997  lighneal  48089  odd2prm2  48209  even3prm2  48210  grictr  48414  grlimgrtrilem2  48493  usgrexmpl12ngric  48529  gpgprismgr4cycllem8  48593  gpgprismgr4cycllem11  48596  pgnbgreunbgrlem2lem1  48605  upgrwlkupwlk  48631  ovn0ssdmfun  48650  islinindfis  48940  rrx2linest  49233  line2ylem  49242  mofeu  49338  homf0  49499  uobffth  49708  uobeqw  49709  initopropd  49733  termopropd  49734  zeroopropd  49735  fucofvalne  49815  isthincd2  49927  lanrcl  50111  ranrcl  50112  setrec2fun  50182  elsetrecslem  50189  setrecsres  50192  secval  50237  cscval  50238  cotval  50239