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  17588  joindmss  18318  meetdmss  18332  gictr  19190  cntzval  19235  symg2bas  19307  odfval  19446  efgsfo  19653  efgrelexlemb  19664  dprddomcld  19917  dprdsubg  19940  dprd2da  19958  lssacs  20905  cnfldinv  21344  pzriprnglem7  21429  ocvval  21609  selvval  22055  dmatmul  22417  mdetfval1  22510  mndifsplit  22556  fvmptnn04if  22769  toprntopon  22845  opnnei  23040  ordtbas2  23111  ordtrest2lem  23123  lmmo  23300  fincmp  23313  bwth  23330  txbas  23487  ptcnplem  23541  tx2ndc  23571  hmphtr  23703  fbun  23760  filconn  23803  ptcmplem5  23976  cnextcn  23987  utoptop  24155  ucncn  24205  metust  24479  cfilucfil  24480  elcncf1di  24821  xrhmeo  24877  phtpycc  24923  copco  24951  pcohtpylem  24952  pcopt  24955  pcopt2  24956  ncvsi  25084  ovolval  25407  iunmbl2  25491  itg2splitlem  25682  cpnfval  25867  plyval  26131  fta1  26249  aaliou2b  26282  tayl0  26302  ulmdvlem3  26344  radcnvlem2  26356  dvradcnv  26363  reeff1o  26390  sincosq1lem  26439  sincosq2sgn  26441  sincosq4sgn  26443  sinq12ge0  26450  logrncl  26509  eflog  26518  cxpge0  26625  logb1  26712  atanf  26823  atanbnd  26869  igamf  26994  igamcl  26995  lgsne0  27279  mul2sq  27363  2sqreultblem  27392  pntibnd  27537  ostth  27583  nobdaymin  27722  nocvxminlem  27723  cutlt  27880  norec2ov  27904  addsuniflem  27948  mulsuniflem  28092  zmulscld  28325  zseo  28349  zs12addscl  28389  mptelee  28875  axlowdimlem9  28930  axlowdimlem12  28933  axcontlem2  28945  axcontlem12  28955  structgrssvtx  29004  structgrssiedg  29005  lpvtx  29048  nbuhgr  29323  nbumgr  29327  nbuhgr2vtx1edgblem  29331  nbgr0edglem  29336  nbgr1vtx  29338  uvtx01vtx  29377  prcliscplgr  29394  cusgrsizeinds  29433  sizusglecusglem2  29443  uhgrvd00  29515  fusgrregdegfi  29550  rusgr1vtxlem  29568  wlkeq  29614  wlk1walk  29619  uspgr2wlkeq  29626  wlklenvclwlk  29634  wlkreslem  29648  wlkdlem2  29662  wlkdlem4  29664  spthonepeq  29732  cyclnumvtx  29780  clwlkclwwlkflem  29983  clwlkclwwlkfolem  29986  clwlkclwwlkf  29987  clwwisshclwws  29994  clwwlkneq0  30008  3wlkdlem6  30144  eupth2eucrct  30196  eupth2lem1  30197  eupth2lem3lem7  30213  frgr3vlem1  30252  frgr3vlem2  30253  frgrncvvdeqlem8  30285  frgrncvvdeqlem9  30286  numclwwlk5  30367  frgrreg  30373  frgrregord013  30374  friendshipgt3  30377  isgrpo  30476  vciOLD  30540  vcex  30557  nmogtmnf  30749  siilem1  30830  siii  30832  ajmoi  30837  bcsiALT  31158  hhcms  31182  ocval  31259  hsupval  31313  omlsilem  31381  h1de2bi  31533  h1de2ctlem  31534  hosubeq0i  31805  adjmo  31811  nmopgtmnf  31847  nlfnval  31860  nmcopex  32008  nmcfnex  32032  riesz4i  32042  riesz1  32044  riesz2  32045  opsqrlem1  32119  superpos  32333  hatomistici  32341  chpssati  32342  mdsymlem3  32384  an42ds  32429  3o1cs  32440  3o2cs  32441  3o3cs  32442  iunrnmptss  32544  brabgaf  32586  f1mptrn  32609  ffsrn  32702  fpwrelmap  32706  xnn0gt0  32742  hashxpe  32782  sgn3da  32809  elrgspnlem4  33212  prmidl2  33405  mxidlnzrb  33444  evl1deg2  33539  evl1deg3  33540  fedgmul  33620  cos9thpiminplylem2  33766  ordtrest2NEWlem  33905  qqhval2  33965  esumfsup  34053  esumcvg  34069  cntnevol  34211  ddemeas  34219  dya2icoseg2  34262  dya2iocnei  34266  eulerpartlems  34344  eulerpartlemgvv  34360  eulerpart  34366  cndprobprob  34422  ballotlemsdom  34496  ballotth  34522  bnj945  34756  bnj1379  34813  bnj1459  34826  bnj557  34884  bnj571  34889  bnj849  34908  bnj964  34926  bnj978  34932  bnj1018g  34946  bnj1018  34947  bnj1020  34948  bnj1033  34952  bnj1175  34987  bnj1398  35017  bnj1417  35024  bnj1523  35054  nummin  35074  onvf1odlem4  35086  onvf1od  35087  cusgr3cyclex  35116  txpconn  35212  satfv1  35343  satffun  35389  msubco  35511  mclsax  35549  setinds  35759  dfon2lem7  35770  dfon2lem8  35771  pprodss4v  35865  fullfunfv  35928  altxpsspw  35958  funtransport  36012  fvtransport  36013  funray  36121  fvray  36122  funline  36123  fvline  36125  finminlem  36299  bisym1  36400  onsucconni  36418  onsucsuccmpi  36424  weiunse  36449  bj-currypara  36541  axc11n11r  36664  bj-equsal2  36806  bj-xpima1snALT  36938  bj-unexg  37019  bj-bm1.3ii  37045  bj-opelidb1ALT  37147  mptsnunlem  37319  iooelexlt  37343  relowlpssretop  37345  rdgeqoa  37351  difunieq  37355  nlpineqsn  37389  fvineqsneq  37393  wl-ax12v2cl  37487  wl-lem-nexmo  37548  matunitlindflem1  37603  ptrecube  37607  poimirlem26  37633  poimirlem30  37637  poimir  37640  ismblfin  37648  itg2addnclem  37658  dvasin  37691  sdclem2  37729  totbndbnd  37776  ismgmOLD  37837  exidresid  37866  isrngo  37884  rngoablo2  37896  rngoueqz  37927  isdivrngo  37937  isdrngo1  37943  isdrngo2  37945  ispridl2  38025  relcnveq3  38302  elrelscnveq3  38475  dmqsblocks  38838  ax12eq  38927  ax12el  38928  lkr0f  39080  hl2at  39392  dalemswapyz  39643  pclfinclN  39937  osumcllem11N  39953  pexmidlem8N  39964  ltrnnid  40123  aks4d1p8  42068  redvmptabs  42341  sn-00id  42382  rictr  42501  eu6w  42657  mptfcl  42701  fphpd  42797  elmnc  43118  itgoval  43143  arearect  43197  reabsifpos  43616  clsk3nimkb  44022  grumnud  44268  nanorxor  44287  pm11.71  44379  iotavalsb  44415  sbiota1  44416  2uasbanh  44544  eel0TT  44686  eelT00  44687  eelTTT  44688  eelT11  44689  eelT12  44691  eelTT1  44692  eelT01  44693  eel0T1  44694  eelTT  44753  uunT1p1  44763  uun121  44765  uun121p1  44766  un2122  44772  uunTT1  44775  uunTT1p1  44776  uunTT1p2  44777  uunT11  44778  uunT11p1  44779  uunT11p2  44780  uunT12  44781  uunT12p1  44782  uunT12p2  44783  uunT12p3  44784  uunT12p4  44785  uunT12p5  44786  uun111  44787  3anidm12p2  44789  uun123  44790  3impdirp1  44798  undif3VD  44864  ax6e2ndeqVD  44891  2uasbanhVD  44893  ax6e2ndeqALT  44913  iunconnlem2  44917  sineq0ALT  44919  modelaxreplem1  44961  permaxrep  44989  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem3  45994  stoweidlem17  46008  fourierdlem42  46140  fourierdlem48  46145  fourierdlem50  46147  fourierdlem51  46148  fourierdlem76  46173  fourierdlem83  46180  fourierdlem87  46184  hoidmvval0  46578  evenwodadd  46879  rexrsb  47094  2reu8i  47107  2reuimp  47109  afv0nbfvbi  47145  afvfv0bi  47146  afveu  47147  fnbrafvb  47148  afvres  47166  tz6.12-afv  47167  dmfcoafv  47169  afvco2  47170  aovprc  47182  aovrcl  47183  aovmpt4g  47195  afv2eu  47232  afv2res  47233  tz6.12-afv2  47234  tz6.12i-afv2  47237  afv2rnfveq  47256  fvmptrab  47286  fvmptrabdm  47287  fzopred  47316  2ffzoeq  47321  elsprel  47469  prproropf1o  47501  reupr  47516  lighneal  47605  odd2prm2  47712  even3prm2  47713  grictr  47916  grlimgrtrilem2  47987  usgrexmpl12ngric  48022  gpgprismgr4cycllem8  48085  gpgprismgr4cycllem11  48088  pgnbgreunbgrlem2lem1  48097  upgrwlkupwlk  48121  ovn0ssdmfun  48140  islinindfis  48431  rrx2linest  48724  line2ylem  48733  mofeu  48829  homf0  48991  uobffth  49200  uobeqw  49201  initopropd  49225  termopropd  49226  zeroopropd  49227  fucofvalne  49307  isthincd2  49419  lanrcl  49603  ranrcl  49604  setrec2fun  49674  elsetrecslem  49681  setrecsres  49684  secval  49729  cscval  49730  cotval  49731