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  nanass  1510  19.38  1839  19.35  1877  19.8aw  2051  equsexv  2269  sbi2  2302  nfeqf2  2375  equsex  2416  dfmoeu  2529  2mo  2641  axie2  2696  necon1bi  2953  necon1i  2958  r19.35  3088  r19.35OLD  3089  sbhypfOLD  3508  spc2ed  3564  reu6  3694  rabssrabd  4042  uneqin  4248  difin0ss  4332  inelcm  4424  rzal  4468  ralf0  4473  falseral0  4475  raaan2  4480  difprsn1  4760  tppreqb  4765  n0snor2el  4793  unissint  4932  intminss  4934  dfiun2g  4990  iununi  5058  triin  5226  bm1.3iiOLD  5252  eusv2nf  5345  reusv3i  5354  moabex  5414  opelopabt  5487  eqrelrel  5751  opeliunxp2  5792  opelrn  5896  ssxpb  6135  xpima  6143  xpimasn  6146  dmsn0el  6172  relcnvtr  6228  relcoi2  6238  elsnxp  6252  reuop  6254  iotanul  6477  f1imadifssran  6586  dffv2  6938  fnfvrnss  7075  fressnfv  7114  fconst5  7162  f1mpt  7218  isocnv3  7289  f1owe  7310  ovprc  7407  fvmpopr2d  7531  onminesb  7749  onminsb  7750  onintrab  7752  onnminsb  7755  ordsuci  7764  onsucuni2  7789  tfindsg2  7818  zfrep6  7913  fo1stres  7973  fo2ndres  7974  bropopvvv  8046  bropfvvvv  8048  frxp  8082  poseq  8114  soseq  8115  opeliunxp2f  8166  mpoxopoveqd  8177  reldmtpos  8190  frrlem4  8245  tfrlem5  8325  tfrlem9  8330  tfr2  8343  rdgsuc  8369  oaordi  8487  oeordi  8528  omopthi  8602  on2recsov  8609  fvmptmap  8831  mptelixpg  8885  ener  8949  domtr  8955  snfiOLD  8992  unen  8994  undom  9006  dom0  9046  xpf1o  9080  mapen  9082  rexdif1enOLD  9100  dif1enOLD  9103  pssnn  9109  unfi  9112  ssfi  9114  ensymfib  9125  entrfil  9126  enfii  9127  domtrfil  9133  unxpdomlem3  9175  isinf  9183  isinfOLD  9184  frfi  9208  unblem1  9215  fofinf1o  9259  fsuppun  9314  inf3lem2  9558  inf3lem5  9561  cantnfp1lem1  9607  cantnfp1lem3  9609  tcmin  9670  frr2  9689  r1ordg  9707  r1ord  9709  rankr1ai  9727  r1val3  9767  bndrank  9770  unbndrank  9771  rankr1b  9793  rankxplim3  9810  tcrank  9813  xpnum  9880  cardmin2  9928  infxpenlem  9942  fseqen  9956  dfac8clem  9961  alephsson  10029  alephfp  10037  dfac4  10051  kmlem6  10085  kmlem8  10087  kmlem9  10088  cflem  10174  infpssr  10237  fin1a2lem12  10340  axcc4  10368  axcc4dom  10370  ac6s2  10415  zornn0g  10434  cardidg  10477  unsnen  10482  pwcfsdom  10512  cfpwsdom  10513  gchpwdom  10599  r1tskina  10711  intgru  10743  indpi  10836  nqereu  10858  supsrlem  11040  letrii  11275  dfnn3  12176  zaddcl  12549  nn0ind  12605  fnn0ind  12609  ublbneg  12868  nn01to3  12876  infmrp1  13281  fz0  13476  fzo1fzo0n0  13652  elfzom1elp1fzo  13669  fzo0end  13695  elfznelfzo  13709  fzind2  13722  injresinjlem  13724  fleqceilz  13792  nnsinds  13929  nn0sinds  13930  faclbnd4lem1  14234  hashinf  14276  hasheqf1oi  14292  hashgt0elex  14342  hashgt23el  14365  hashfacen  14395  hash2prde  14411  hash2sspr  14430  fun2dmnop0  14445  iswrddm0  14479  swrdnnn0nd  14597  swrdnd0  14598  swrdlsw  14608  pfxn0  14627  pfxnd0  14629  swrdswrdlem  14645  pfxccatin12lem3  14673  pfxccat3  14675  pfxccat3a  14679  swrdccat3blem  14680  cshwsublen  14737  cshwidxmod  14744  repswcshw  14753  cshw1  14763  trclun  14956  dmtrclfv  14960  rediv  15073  imdiv  15080  fsump1i  15711  modfsummods  15735  bpolydiflem  15996  bpoly3  16000  bpoly4  16001  cos1bnd  16131  sinltx  16133  rpnnen2lem1  16158  rpnnen2lem2  16159  rpnnen2lem12  16169  odd2np1  16287  opoe  16309  omoe  16310  opeo  16311  omeo  16312  gcdcllem1  16445  gcdaddmlem  16470  dfgcd2  16492  algfx  16526  lcmledvds  16545  lcmfunsnlem  16587  lcmfun  16591  coprmprod  16607  coprmproddvdslem  16608  odzval  16738  odzdvds  16742  prmreclem5  16867  mul4sq  16901  prmgaplem5  17002  prmgaplem6  17003  imasaddfnlem  17467  mreexexlem4d  17584  joindmss  18314  meetdmss  18328  gictr  19184  cntzval  19229  symg2bas  19299  odfval  19438  efgsfo  19645  efgrelexlemb  19656  dprddomcld  19909  dprdsubg  19932  dprd2da  19950  lssacs  20849  cnfldinv  21290  pzriprnglem7  21373  ocvval  21552  selvval  21998  dmatmul  22360  mdetfval1  22453  mndifsplit  22499  fvmptnn04if  22712  toprntopon  22788  opnnei  22983  ordtbas2  23054  ordtrest2lem  23066  lmmo  23243  fincmp  23256  bwth  23273  txbas  23430  ptcnplem  23484  tx2ndc  23514  hmphtr  23646  fbun  23703  filconn  23746  ptcmplem5  23919  cnextcn  23930  utoptop  24098  ucncn  24148  metust  24422  cfilucfil  24423  elcncf1di  24764  xrhmeo  24820  phtpycc  24866  copco  24894  pcohtpylem  24895  pcopt  24898  pcopt2  24899  ncvsi  25027  ovolval  25350  iunmbl2  25434  itg2splitlem  25625  cpnfval  25810  plyval  26074  fta1  26192  aaliou2b  26225  tayl0  26245  ulmdvlem3  26287  radcnvlem2  26299  dvradcnv  26306  reeff1o  26333  sincosq1lem  26382  sincosq2sgn  26384  sincosq4sgn  26386  sinq12ge0  26393  logrncl  26452  eflog  26461  cxpge0  26568  logb1  26655  atanf  26766  atanbnd  26812  igamf  26937  igamcl  26938  lgsne0  27222  mul2sq  27306  2sqreultblem  27335  pntibnd  27480  ostth  27526  nocvxminlem  27665  nocvxmin  27666  cutlt  27816  norec2ov  27840  addsuniflem  27884  mulsuniflem  28028  zmulscld  28261  zseo  28284  mptelee  28798  axlowdimlem9  28853  axlowdimlem12  28856  axcontlem2  28868  axcontlem12  28878  structgrssvtx  28927  structgrssiedg  28928  lpvtx  28971  nbuhgr  29246  nbumgr  29250  nbuhgr2vtx1edgblem  29254  nbgr0edglem  29259  nbgr1vtx  29261  uvtx01vtx  29300  prcliscplgr  29317  cusgrsizeinds  29356  sizusglecusglem2  29366  uhgrvd00  29438  fusgrregdegfi  29473  rusgr1vtxlem  29491  wlkeq  29537  wlk1walk  29542  uspgr2wlkeq  29549  wlklenvclwlk  29557  wlkreslem  29571  wlkdlem2  29585  wlkdlem4  29587  spthonepeq  29655  cyclnumvtx  29703  clwlkclwwlkflem  29906  clwlkclwwlkfolem  29909  clwlkclwwlkf  29910  clwwisshclwws  29917  clwwlkneq0  29931  3wlkdlem6  30067  eupth2eucrct  30119  eupth2lem1  30120  eupth2lem3lem7  30136  frgr3vlem1  30175  frgr3vlem2  30176  frgrncvvdeqlem8  30208  frgrncvvdeqlem9  30209  numclwwlk5  30290  frgrreg  30296  frgrregord013  30297  friendshipgt3  30300  isgrpo  30399  vciOLD  30463  vcex  30480  nmogtmnf  30672  siilem1  30753  siii  30755  ajmoi  30760  bcsiALT  31081  hhcms  31105  ocval  31182  hsupval  31236  omlsilem  31304  h1de2bi  31456  h1de2ctlem  31457  hosubeq0i  31728  adjmo  31734  nmopgtmnf  31770  nlfnval  31783  nmcopex  31931  nmcfnex  31955  riesz4i  31965  riesz1  31967  riesz2  31968  opsqrlem1  32042  superpos  32256  hatomistici  32264  chpssati  32265  mdsymlem3  32307  an42ds  32352  3o1cs  32363  3o2cs  32364  3o3cs  32365  iunrnmptss  32467  brabgaf  32509  f1mptrn  32532  ffsrn  32625  fpwrelmap  32629  xnn0gt0  32665  hashxpe  32705  sgn3da  32732  elrgspnlem4  33169  prmidl2  33385  mxidlnzrb  33424  evl1deg2  33519  evl1deg3  33520  fedgmul  33600  cos9thpiminplylem2  33746  ordtrest2NEWlem  33885  qqhval2  33945  esumfsup  34033  esumcvg  34049  cntnevol  34191  ddemeas  34199  dya2icoseg2  34242  dya2iocnei  34246  eulerpartlems  34324  eulerpartlemgvv  34340  eulerpart  34346  cndprobprob  34402  ballotlemsdom  34476  ballotth  34502  bnj945  34736  bnj1379  34793  bnj1459  34806  bnj557  34864  bnj571  34869  bnj849  34888  bnj964  34906  bnj978  34912  bnj1018g  34926  bnj1018  34927  bnj1020  34928  bnj1033  34932  bnj1175  34967  bnj1398  34997  bnj1417  35004  bnj1523  35034  nummin  35054  onvf1odlem4  35066  onvf1od  35067  cusgr3cyclex  35096  txpconn  35192  satfv1  35323  satffun  35369  msubco  35491  mclsax  35529  setinds  35739  dfon2lem7  35750  dfon2lem8  35751  pprodss4v  35845  fullfunfv  35908  altxpsspw  35938  funtransport  35992  fvtransport  35993  funray  36101  fvray  36102  funline  36103  fvline  36105  finminlem  36279  bisym1  36380  onsucconni  36398  onsucsuccmpi  36404  weiunse  36429  bj-currypara  36521  axc11n11r  36644  bj-equsal2  36786  bj-xpima1snALT  36918  bj-unexg  36999  bj-bm1.3ii  37025  bj-opelidb1ALT  37127  mptsnunlem  37299  iooelexlt  37323  relowlpssretop  37325  rdgeqoa  37331  difunieq  37335  nlpineqsn  37369  fvineqsneq  37373  wl-ax12v2cl  37467  wl-lem-nexmo  37528  matunitlindflem1  37583  ptrecube  37587  poimirlem26  37613  poimirlem30  37617  poimir  37620  ismblfin  37628  itg2addnclem  37638  dvasin  37671  sdclem2  37709  totbndbnd  37756  ismgmOLD  37817  exidresid  37846  isrngo  37864  rngoablo2  37876  rngoueqz  37907  isdivrngo  37917  isdrngo1  37923  isdrngo2  37925  ispridl2  38005  relcnveq3  38282  elrelscnveq3  38455  dmqsblocks  38818  ax12eq  38907  ax12el  38908  lkr0f  39060  hl2at  39372  dalemswapyz  39623  pclfinclN  39917  osumcllem11N  39933  pexmidlem8N  39944  ltrnnid  40103  aks4d1p8  42048  redvmptabs  42321  sn-00id  42362  rictr  42481  eu6w  42637  mptfcl  42681  fphpd  42777  elmnc  43098  itgoval  43123  arearect  43177  reabsifpos  43596  clsk3nimkb  44002  grumnud  44248  nanorxor  44267  pm11.71  44359  iotavalsb  44395  sbiota1  44396  2uasbanh  44524  eel0TT  44666  eelT00  44667  eelTTT  44668  eelT11  44669  eelT12  44671  eelTT1  44672  eelT01  44673  eel0T1  44674  eelTT  44733  uunT1p1  44743  uun121  44745  uun121p1  44746  un2122  44752  uunTT1  44755  uunTT1p1  44756  uunTT1p2  44757  uunT11  44758  uunT11p1  44759  uunT11p2  44760  uunT12  44761  uunT12p1  44762  uunT12p2  44763  uunT12p3  44764  uunT12p4  44765  uunT12p5  44766  uun111  44767  3anidm12p2  44769  uun123  44770  3impdirp1  44778  undif3VD  44844  ax6e2ndeqVD  44871  2uasbanhVD  44873  ax6e2ndeqALT  44893  iunconnlem2  44897  sineq0ALT  44899  modelaxreplem1  44941  permaxrep  44969  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem3  45974  stoweidlem17  45988  fourierdlem42  46120  fourierdlem48  46125  fourierdlem50  46127  fourierdlem51  46128  fourierdlem76  46153  fourierdlem83  46160  fourierdlem87  46164  hoidmvval0  46558  evenwodadd  46859  rexrsb  47074  2reu8i  47087  2reuimp  47089  afv0nbfvbi  47125  afvfv0bi  47126  afveu  47127  fnbrafvb  47128  afvres  47146  tz6.12-afv  47147  dmfcoafv  47149  afvco2  47150  aovprc  47162  aovrcl  47163  aovmpt4g  47175  afv2eu  47212  afv2res  47213  tz6.12-afv2  47214  tz6.12i-afv2  47217  afv2rnfveq  47236  fvmptrab  47266  fvmptrabdm  47267  fzopred  47296  2ffzoeq  47301  elsprel  47449  prproropf1o  47481  reupr  47496  lighneal  47585  odd2prm2  47692  even3prm2  47693  grictr  47896  grlimgrtrilem2  47967  usgrexmpl12ngric  48002  gpgprismgr4cycllem8  48065  gpgprismgr4cycllem11  48068  pgnbgreunbgrlem2lem1  48077  upgrwlkupwlk  48101  ovn0ssdmfun  48120  islinindfis  48411  rrx2linest  48704  line2ylem  48713  mofeu  48809  homf0  48971  uobffth  49180  uobeqw  49181  initopropd  49205  termopropd  49206  zeroopropd  49207  fucofvalne  49287  isthincd2  49399  lanrcl  49583  ranrcl  49584  setrec2fun  49654  elsetrecslem  49661  setrecsres  49664  secval  49709  cscval  49710  cotval  49711