Theorem sylbir 238

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3i  294  ex  418  3expa  1136  3ori  1451  an42ds  1520  nanass  1540  19.38  1872  19.35  1910  19.8aw  2085  sbrimvw  2128  equsexv  2306  sbi2  2339  nfeqf2  2411  equsex  2452  dfmoeu  2565  2mo  2678  axie2  2732  necon1bi  2988  necon1i  2993  r19.35  3125  spc2ed  3562  reu6  3691  rabssrabd  4038  uneqin  4242  difin0ss  4328  inelcm  4425  falseral0OLD  4478  raaan2  4485  difprsn1  4770  tppreqb  4775  n0snor2el  4800  unissint  4939  intminss  4941  dfiun2g  4996  iununi  5067  triin  5237  bm1.3iiOLD  5267  eusv2nf  5368  reusv3i  5377  axprglem  5409  axprg  5410  moabexOLD  5442  opelopabt  5518  eqrelrel  5785  opeliunxp2  5826  opelrn  5935  ssxpb  6174  xpima  6182  xpimasn  6185  dmsn0el  6214  relcnvtrOLD  6272  relcoi2  6282  elsnxp  6296  reuop  6298  iotanul  6520  dffv2  6980  fnfvrnss  7120  fressnfv  7163  fconst5  7211  f1mpt  7264  isocnv3  7339  f1owe  7360  f1oweOLD  7361  ovprc  7457  fvmpopr2d  7581  ovn0ssdmfun  7588  onminesb  7798  onminsb  7799  onintrab  7801  onnminsb  7804  ordsuci  7813  onsucuni2  7836  tfindsg2  7864  zfrep6OLD  7958  fo1stres  8018  fo2ndres  8019  bropopvvv  8091  bropfvvvv  8093  frxp  8128  poseq  8160  soseq  8161  opeliunxp2f  8212  mpoxopoveqd  8223  reldmtpos  8236  frrlem4  8292  tfrlem5  8372  tfrlem9  8378  tfr2  8391  rdgsuc  8417  oaordi  8537  oeordi  8579  omopthi  8653  on2recsov  8660  fvmptmap  8885  mptelixpg  8939  ener  9004  domtr  9010  unen  9049  undom  9060  dom0  9100  xpf1o  9134  mapen  9136  pssnn  9160  unfi  9162  ssfi  9164  ensymfib  9175  entrfil  9176  enfii  9177  domtrfil  9183  unxpdomlem3  9225  isinf  9232  frfi  9252  unblem1  9259  fofinf1o  9296  fsuppun  9354  elirrvOLD  9567  inf3lem2  9605  inf3lem5  9608  cantnfp1lem1  9654  cantnfp1lem3  9656  tcmin  9715  setinds  9725  frr2  9739  r1ordg  9757  r1ord  9759  rankr1ai  9777  r1val3  9817  bndrank  9820  unbndrank  9821  rankr1b  9843  rankxplim3  9860  tcrank  9863  xpnum  9953  cardmin2  10001  infxpenlem  10013  fseqen  10027  dfac8clem  10032  alephsson  10100  alephfp  10108  dfac4  10122  kmlem6  10155  kmlem8  10157  kmlem9  10158  cflem  10244  infpssr  10307  fin1a2lem12  10410  axcc4  10438  axcc4dom  10440  ac6s2  10485  zornn0g  10504  cardidg  10549  unsnen  10554  pwcfsdom  10585  cfpwsdom  10586  gchpwdom  10672  r1tskina  10784  intgru  10816  indpi  10909  nqereu  10931  supsrlem  11113  letrii  11352  dfnn3  12264  zaddcl  12651  nn0ind  12709  fnn0ind  12713  ublbneg  12975  nn01to3  12983  infmrp1  13389  fz0  13585  fzo1fzo0n0  13763  elfzom1elp1fzo  13780  fzo0end  13806  elfznelfzo  13821  fzind2  13836  injresinjlem  13838  fleqceilz  13907  nnsinds  14044  nn0sinds  14045  faclbnd4lem1  14349  hashinf  14391  hasheqf1oi  14407  hashgt0elex  14457  hashgt23el  14481  hashfacen  14511  hash2prde  14527  hash2sspr  14546  fun2dmnop0  14561  iswrddm0  14595  swrdnnn0nd  14718  swrdnd0  14719  swrdlsw  14729  pfxn0  14748  pfxnd0  14750  swrdswrdlem  14765  pfxccatin12lem3  14793  pfxccat3  14795  pfxccat3a  14799  swrdccat3blem  14800  cshwsublen  14859  cshwidxmod  14866  repswcshw  14875  cshw1  14885  trclun  15077  dmtrclfv  15081  sgn3da  15164  rediv  15208  imdiv  15215  fsump1i  15845  modfsummods  15870  bpolydiflem  16132  bpoly3  16136  bpoly4  16137  cos1bnd  16267  sinltx  16269  rpnnen2lem1  16294  rpnnen2lem2  16295  rpnnen2lem12  16305  odd2np1  16423  opoe  16445  omoe  16446  opeo  16447  omeo  16448  gcdcllem1  16581  gcdaddmlem  16606  dfgcd2  16628  algfx  16662  lcmledvds  16681  lcmfunsnlem  16723  lcmfun  16727  coprmprod  16743  coprmproddvdslem  16744  odzval  16875  odzdvds  16879  prmreclem5  17004  mul4sq  17038  prmgaplem5  17139  prmgaplem6  17140  imasaddfnlem  17606  mreexexlem4d  17727  joindmss  18457  meetdmss  18471  gictr  19392  cntzval  19437  symg2bas  19509  odfval  19648  efgsfo  19855  efgrelexlemb  19866  dprddomcld  20119  dprdsubg  20142  dprd2da  20160  rictr  20652  isdrng3lem1  20903  isdrng3  20905  lssacs  21140  prmidl2  21518  cnfldinv  21605  pzriprnglem7  21689  ocvval  21869  selvval  22323  dmatmul  22706  mdetfval1  22799  mndifsplit  22845  fvmptnn04if  23058  toprntopon  23134  opnnei  23329  ordtbas2  23400  ordtrest2lem  23412  lmmo  23589  fincmp  23602  bwth  23619  txbas  23777  ptcnplem  23831  tx2ndc  23861  hmphtr  23993  fbun  24050  filconn  24093  ptcmplem5  24266  cnextcn  24277  utoptop  24444  ucncn  24494  metust  24768  cfilucfil  24769  elcncf1di  25107  xrhmeo  25158  phtpycc  25203  copco  25230  pcohtpylem  25231  pcopt  25234  pcopt2  25235  ncvsi  25363  ovolval  25685  iunmbl2  25769  itg2splitlem  25960  cpnfval  26144  plyval  26403  fta1  26522  aaliou2b  26557  tayl0  26578  ulmdvlem3  26618  radcnvlem2  26630  dvradcnv  26637  reeff1o  26663  sincosq1lem  26715  sincosq2sgn  26717  sincosq4sgn  26719  sinq12ge0  26726  logrncl  26785  eflog  26794  cxpge0  26901  logb1  26987  atanf  27098  atanbnd  27144  igamf  27268  igamcl  27269  lgsne0  27552  mul2sq  27636  2sqreultblem  27665  pntibnd  27810  ostth  27856  nobdaymin  27999  nocvxminlem  28000  cutlt  28178  norec2ov  28203  addsuniflem  28247  mulsuniflem  28395  oldfib  28623  zmulscld  28643  zseo  28668  z12addscl  28723  mpteleeOLD  29302  axlowdimlem9  29357  axlowdimlem12  29360  axcontlem2  29372  axcontlem12  29382  structgrssvtx  29431  structgrssiedg  29432  lpvtx  29475  nbuhgr  29753  nbumgr  29757  nbuhgr2vtx1edgblem  29761  nbgr0edglem  29766  nbgr1vtx  29768  uvtx01vtx  29807  prcliscplgr  29824  cusgrsizeinds  29862  sizusglecusglem2  29872  uhgrvd00  29944  fusgrregdegfi  29979  rusgr1vtxlem  29997  wlkeq  30043  wlk1walk  30048  uspgr2wlkeq  30055  wlklenvclwlk  30063  wlkreslem  30077  wlkdlem2  30091  wlkdlem4  30093  spthonepeq  30167  cyclnumvtx  30217  clwlkclwwlkflem  30424  clwlkclwwlkfolem  30427  clwlkclwwlkf  30428  clwwisshclwws  30435  clwwlkneq0  30449  3wlkdlem6  30589  eupth2eucrct  30641  eupth2lem1  30642  eupth2lem3lem7  30658  frgr3vlem1  30697  frgr3vlem2  30698  frgrncvvdeqlem8  30730  frgrncvvdeqlem9  30731  numclwwlk5  30812  frgrreg  30818  frgrregord013  30819  friendshipgt3  30822  isgrpo  30922  vciOLD  30986  vcex  31003  nmogtmnf  31195  siilem1  31276  siii  31278  ajmoi  31283  bcsiALT  31604  hhcms  31628  ocval  31705  hsupval  31759  omlsilem  31827  h1de2bi  31979  h1de2ctlem  31980  hosubeq0i  32251  adjmo  32257  nmopgtmnf  32293  nlfnval  32306  nmcopex  32454  nmcfnex  32478  riesz4i  32488  riesz1  32490  riesz2  32491  opsqrlem1  32565  superpos  32779  hatomistici  32787  chpssati  32788  mdsymlem3  32830  3o1cs  32882  3o2cs  32883  3o3cs  32884  iunrnmptss  32983  brabgaf  33024  f1mptrn  33053  ffsrn  33145  xnn0gt0  33186  hashxpe  33224  elrgspnlem4  33631  mxidlnzrb  33828  evl1deg2  33933  evl1deg3  33934  fedgmul  34087  cos9thpiminplylem2  34239  ordtrest2NEWlem  34378  qqhval2  34438  esumfsup  34526  esumcvg  34542  cntnevol  34685  ddemeas  34693  dya2icoseg2  34735  dya2iocnei  34739  eulerpartlems  34817  eulerpartlemgvv  34833  eulerpart  34839  cndprobprob  34895  ballotlemsdom  34969  ballotth  34995  bnj945  35229  bnj1379  35285  bnj1459  35298  bnj557  35356  bnj571  35361  bnj849  35380  bnj964  35398  bnj978  35404  bnj1018g  35418  bnj1018  35419  bnj1020  35420  bnj1033  35424  bnj1175  35459  bnj1398  35489  bnj1417  35496  bnj1523  35526  nummin  35544  r1omhf  35560  axprALT2  35563  fineqvnttrclselem1  35593  rankkardu  35643  onvf1odlem4  35649  onvf1od  35650  vonf1osev  35655  vonf1oonfo  35658  cusgr3cyclex  35671  txpconn  35763  satfv1  35894  satffun  35940  msubco  36062  mclsax  36100  dfon2lem7  36318  dfon2lem8  36319  pprodss4v  36413  fullfunfv  36478  altxpsspw  36508  funtransport  36562  fvtransport  36563  funray  36671  fvray  36672  funline  36673  fvline  36675  finminlem  36888  bisym1  36989  onsucconni  37007  onsucsuccmpi  37013  weiunse  37038  bj-currypara  37211  bj-cbvaw  37322  axc11n11r  37367  bj-equsal2  37519  bj-xpima1snALT  37652  bj-unexg  37733  bj-bm1.3ii  37759  bj-axseprep  37770  bj-axreprepsep  37771  bj-opelidb1ALT  37869  mptsnunlem  38043  iooelexlt  38067  relowlpssretop  38069  rdgeqoa  38075  difunieq  38079  nlpineqsn  38113  fvineqsneq  38117  wl-ax12v2cl  38211  wl-lem-nexmo  38281  matunitlindflem1  38326  ptrecube  38330  poimirlem26  38356  poimirlem30  38360  poimir  38363  ismblfin  38371  itg2addnclem  38381  dvasin  38414  sdclem2  38453  totbndbnd  38500  ismgmOLD  38561  exidresid  38590  isrngo  38608  rngoablo2  38620  rngoueqz  38651  isdivrngo  38661  isdrngo1  38667  isdrngo2  38669  ispridl2  38749  relcnveq3  39036  elrelscnveq3  39336  disjimeceqim  39513  dmqsblocks  39676  ax12eq  39775  ax12el  39776  lkr0f  39928  hl2at  40239  dalemswapyz  40490  pclfinclN  40784  osumcllem11N  40800  pexmidlem8N  40811  ltrnnid  40970  aks4d1p8  42914  redvmptabs  43181  sn-00id  43222  eu6w  43468  mptfcl  43511  fphpd  43603  elmnc  43923  itgoval  43948  arearect  44002  reabsifpos  44420  clsk3nimkb  44826  grumnud  45056  nanorxor  45075  pm11.71  45167  iotavalsb  45203  sbiota1  45204  2uasbanh  45330  eel0TT  45472  eelT00  45473  eelTTT  45474  eelT11  45475  eelT12  45477  eelTT1  45478  eelT01  45479  eel0T1  45480  eelTT  45539  uunT1p1  45549  uun121  45551  uun121p1  45552  un2122  45558  uunTT1  45561  uunTT1p1  45562  uunTT1p2  45563  uunT11  45564  uunT11p1  45565  uunT11p2  45566  uunT12  45567  uunT12p1  45568  uunT12p2  45569  uunT12p3  45570  uunT12p4  45571  uunT12p5  45572  uun111  45573  3anidm12p2  45575  uun123  45576  3impdirp1  45584  undif3VD  45650  ax6e2ndeqVD  45677  2uasbanhVD  45679  ax6e2ndeqALT  45699  iunconnlem2  45703  sineq0ALT  45705  modelaxreplem1  45747  permaxrep  45775  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  stoweidlem3  46777  stoweidlem17  46791  fourierdlem42  46923  fourierdlem48  46928  fourierdlem50  46930  fourierdlem51  46931  fourierdlem76  46956  fourierdlem83  46963  fourierdlem87  46967  hoidmvval0  47361  evenwodadd  47662  rexrsb  47897  2reu8i  47910  2reuimp  47912  afv0nbfvbi  47948  afvfv0bi  47949  afveu  47950  fnbrafvb  47951  afvres  47969  tz6.12-afv  47970  dmfcoafv  47972  afvco2  47973  aovprc  47985  aovrcl  47986  aovmpt4g  47998  afv2eu  48035  afv2res  48036  tz6.12-afv2  48037  tz6.12i-afv2  48040  afv2rnfveq  48059  fvmptrab  48089  fvmptrabdm  48090  fzopred  48120  2ffzoeq  48125  muldvdsfacm1  48184  elsprel  48284  prproropf1o  48316  reupr  48331  lighneal  48423  odd2prm2  48543  even3prm2  48544  grictr  48748  grlimgrtrilem2  48827  usgrexmpl12ngric  48863  gpgprismgr4cycllem8  48927  gpgprismgr4cycllem11  48930  pgnbgreunbgrlem2lem1  48939  upgrwlkupwlk  48965  islinindfis  49288  rrx2linest  49581  line2ylem  49590  mofeu  49685  homf0  49846  uobffth  50055  uobeqw  50056  initopropd  50080  termopropd  50081  zeroopropd  50082  fucofvalne  50162  isthincd2  50274  lanrcl  50458  ranrcl  50459  setrec2fun  50529  elsetrecslem  50536  setrecsres  50539  secval  50584  cscval  50585  cotval  50586