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  2376  equsex  2417  dfmoeu  2530  2mo  2642  axie2  2697  necon1bi  2954  necon1i  2959  r19.35  3089  r19.35OLD  3090  sbhypfOLD  3514  spc2ed  3570  reu6  3700  rabssrabd  4049  uneqin  4255  difin0ss  4339  inelcm  4431  rzal  4475  ralf0  4480  falseral0  4482  raaan2  4487  difprsn1  4767  tppreqb  4772  n0snor2el  4800  unissint  4939  intminss  4941  dfiun2g  4997  iununi  5066  triin  5234  bm1.3iiOLD  5260  eusv2nf  5353  reusv3i  5362  moabex  5422  opelopabt  5495  eqrelrel  5763  opeliunxp2  5805  opelrn  5910  ssxpb  6150  xpima  6158  xpimasn  6161  dmsn0el  6187  relcnvtr  6243  relcoi2  6253  elsnxp  6267  reuop  6269  iotanul  6492  f1imadifssran  6605  dffv2  6959  fnfvrnss  7096  fressnfv  7135  fconst5  7183  f1mpt  7239  isocnv3  7310  f1owe  7331  ovprc  7428  fvmpopr2d  7554  onminesb  7772  onminsb  7773  onintrab  7775  onnminsb  7778  ordsuci  7787  onsucuni2  7812  tfindsg2  7841  zfrep6  7936  fo1stres  7997  fo2ndres  7998  bropopvvv  8072  bropfvvvv  8074  frxp  8108  poseq  8140  soseq  8141  opeliunxp2f  8192  mpoxopoveqd  8203  reldmtpos  8216  frrlem4  8271  tfrlem5  8351  tfrlem9  8356  tfr2  8369  rdgsuc  8395  oaordi  8513  oeordi  8554  omopthi  8628  on2recsov  8635  fvmptmap  8857  mptelixpg  8911  ener  8975  domtr  8981  snfiOLD  9018  unen  9020  undom  9033  dom0  9075  xpf1o  9109  mapen  9111  rexdif1enOLD  9129  dif1enOLD  9132  pssnn  9138  unfi  9141  ssfi  9143  ensymfib  9154  entrfil  9155  enfii  9156  domtrfil  9162  unxpdomlem3  9206  isinf  9214  isinfOLD  9215  frfi  9239  unblem1  9246  fofinf1o  9290  fsuppun  9345  inf3lem2  9589  inf3lem5  9592  cantnfp1lem1  9638  cantnfp1lem3  9640  tcmin  9701  frr2  9720  r1ordg  9738  r1ord  9740  rankr1ai  9758  r1val3  9798  bndrank  9801  unbndrank  9802  rankr1b  9824  rankxplim3  9841  tcrank  9844  xpnum  9911  cardmin2  9959  infxpenlem  9973  fseqen  9987  dfac8clem  9992  alephsson  10060  alephfp  10068  dfac4  10082  kmlem6  10116  kmlem8  10118  kmlem9  10119  cflem  10205  infpssr  10268  fin1a2lem12  10371  axcc4  10399  axcc4dom  10401  ac6s2  10446  zornn0g  10465  cardidg  10508  unsnen  10513  pwcfsdom  10543  cfpwsdom  10544  gchpwdom  10630  r1tskina  10742  intgru  10774  indpi  10867  nqereu  10889  supsrlem  11071  letrii  11306  dfnn3  12207  zaddcl  12580  nn0ind  12636  fnn0ind  12640  ublbneg  12899  nn01to3  12907  infmrp1  13312  fz0  13507  fzo1fzo0n0  13683  elfzom1elp1fzo  13700  fzo0end  13726  elfznelfzo  13740  fzind2  13753  injresinjlem  13755  fleqceilz  13823  nnsinds  13960  nn0sinds  13961  faclbnd4lem1  14265  hashinf  14307  hasheqf1oi  14323  hashgt0elex  14373  hashgt23el  14396  hashfacen  14426  hash2prde  14442  hash2sspr  14461  fun2dmnop0  14476  iswrddm0  14510  swrdnnn0nd  14628  swrdnd0  14629  swrdlsw  14639  pfxn0  14658  pfxnd0  14660  swrdswrdlem  14676  pfxccatin12lem3  14704  pfxccat3  14706  pfxccat3a  14710  swrdccat3blem  14711  cshwsublen  14768  cshwidxmod  14775  repswcshw  14784  cshw1  14794  trclun  14987  dmtrclfv  14991  rediv  15104  imdiv  15111  fsump1i  15742  modfsummods  15766  bpolydiflem  16027  bpoly3  16031  bpoly4  16032  cos1bnd  16162  sinltx  16164  rpnnen2lem1  16189  rpnnen2lem2  16190  rpnnen2lem12  16200  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  gcdcllem1  16476  gcdaddmlem  16501  dfgcd2  16523  algfx  16557  lcmledvds  16576  lcmfunsnlem  16618  lcmfun  16622  coprmprod  16638  coprmproddvdslem  16639  odzval  16769  odzdvds  16773  prmreclem5  16898  mul4sq  16932  prmgaplem5  17033  prmgaplem6  17034  imasaddfnlem  17498  mreexexlem4d  17615  joindmss  18345  meetdmss  18359  gictr  19215  cntzval  19260  symg2bas  19330  odfval  19469  efgsfo  19676  efgrelexlemb  19687  dprddomcld  19940  dprdsubg  19963  dprd2da  19981  lssacs  20880  cnfldinv  21321  pzriprnglem7  21404  ocvval  21583  selvval  22029  dmatmul  22391  mdetfval1  22484  mndifsplit  22530  fvmptnn04if  22743  toprntopon  22819  opnnei  23014  ordtbas2  23085  ordtrest2lem  23097  lmmo  23274  fincmp  23287  bwth  23304  txbas  23461  ptcnplem  23515  tx2ndc  23545  hmphtr  23677  fbun  23734  filconn  23777  ptcmplem5  23950  cnextcn  23961  utoptop  24129  ucncn  24179  metust  24453  cfilucfil  24454  elcncf1di  24795  xrhmeo  24851  phtpycc  24897  copco  24925  pcohtpylem  24926  pcopt  24929  pcopt2  24930  ncvsi  25058  ovolval  25381  iunmbl2  25465  itg2splitlem  25656  cpnfval  25841  plyval  26105  fta1  26223  aaliou2b  26256  tayl0  26276  ulmdvlem3  26318  radcnvlem2  26330  dvradcnv  26337  reeff1o  26364  sincosq1lem  26413  sincosq2sgn  26415  sincosq4sgn  26417  sinq12ge0  26424  logrncl  26483  eflog  26492  cxpge0  26599  logb1  26686  atanf  26797  atanbnd  26843  igamf  26968  igamcl  26969  lgsne0  27253  mul2sq  27337  2sqreultblem  27366  pntibnd  27511  ostth  27557  nocvxminlem  27696  nocvxmin  27697  cutlt  27847  norec2ov  27871  addsuniflem  27915  mulsuniflem  28059  zmulscld  28292  zseo  28315  mptelee  28829  axlowdimlem9  28884  axlowdimlem12  28887  axcontlem2  28899  axcontlem12  28909  structgrssvtx  28958  structgrssiedg  28959  lpvtx  29002  nbuhgr  29277  nbumgr  29281  nbuhgr2vtx1edgblem  29285  nbgr0edglem  29290  nbgr1vtx  29292  uvtx01vtx  29331  prcliscplgr  29348  cusgrsizeinds  29387  sizusglecusglem2  29397  uhgrvd00  29469  fusgrregdegfi  29504  rusgr1vtxlem  29522  wlkeq  29569  wlk1walk  29574  uspgr2wlkeq  29581  wlklenvclwlk  29590  wlkreslem  29604  wlkdlem2  29618  wlkdlem4  29620  spthonepeq  29689  cyclnumvtx  29737  clwlkclwwlkflem  29940  clwlkclwwlkfolem  29943  clwlkclwwlkf  29944  clwwisshclwws  29951  clwwlkneq0  29965  3wlkdlem6  30101  eupth2eucrct  30153  eupth2lem1  30154  eupth2lem3lem7  30170  frgr3vlem1  30209  frgr3vlem2  30210  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  numclwwlk5  30324  frgrreg  30330  frgrregord013  30331  friendshipgt3  30334  isgrpo  30433  vciOLD  30497  vcex  30514  nmogtmnf  30706  siilem1  30787  siii  30789  ajmoi  30794  bcsiALT  31115  hhcms  31139  ocval  31216  hsupval  31270  omlsilem  31338  h1de2bi  31490  h1de2ctlem  31491  hosubeq0i  31762  adjmo  31768  nmopgtmnf  31804  nlfnval  31817  nmcopex  31965  nmcfnex  31989  riesz4i  31999  riesz1  32001  riesz2  32002  opsqrlem1  32076  superpos  32290  hatomistici  32298  chpssati  32299  mdsymlem3  32341  an42ds  32386  3o1cs  32397  3o2cs  32398  3o3cs  32399  iunrnmptss  32501  brabgaf  32543  f1mptrn  32566  ffsrn  32659  fpwrelmap  32663  xnn0gt0  32699  hashxpe  32739  sgn3da  32766  elrgspnlem4  33203  prmidl2  33419  mxidlnzrb  33458  evl1deg2  33553  evl1deg3  33554  fedgmul  33634  cos9thpiminplylem2  33780  ordtrest2NEWlem  33919  qqhval2  33979  esumfsup  34067  esumcvg  34083  cntnevol  34225  ddemeas  34233  dya2icoseg2  34276  dya2iocnei  34280  eulerpartlems  34358  eulerpartlemgvv  34374  eulerpart  34380  cndprobprob  34436  ballotlemsdom  34510  ballotth  34536  bnj945  34770  bnj1379  34827  bnj1459  34840  bnj557  34898  bnj571  34903  bnj849  34922  bnj964  34940  bnj978  34946  bnj1018g  34960  bnj1018  34961  bnj1020  34962  bnj1033  34966  bnj1175  35001  bnj1398  35031  bnj1417  35038  bnj1523  35068  nummin  35088  onvf1odlem4  35100  onvf1od  35101  cusgr3cyclex  35130  txpconn  35226  satfv1  35357  satffun  35403  msubco  35525  mclsax  35563  setinds  35773  dfon2lem7  35784  dfon2lem8  35785  pprodss4v  35879  fullfunfv  35942  altxpsspw  35972  funtransport  36026  fvtransport  36027  funray  36135  fvray  36136  funline  36137  fvline  36139  finminlem  36313  bisym1  36414  onsucconni  36432  onsucsuccmpi  36438  weiunse  36463  bj-currypara  36555  axc11n11r  36678  bj-equsal2  36820  bj-xpima1snALT  36952  bj-unexg  37033  bj-bm1.3ii  37059  bj-opelidb1ALT  37161  mptsnunlem  37333  iooelexlt  37357  relowlpssretop  37359  rdgeqoa  37365  difunieq  37369  nlpineqsn  37403  fvineqsneq  37407  wl-ax12v2cl  37501  wl-lem-nexmo  37562  matunitlindflem1  37617  ptrecube  37621  poimirlem26  37647  poimirlem30  37651  poimir  37654  ismblfin  37662  itg2addnclem  37672  dvasin  37705  sdclem2  37743  totbndbnd  37790  ismgmOLD  37851  exidresid  37880  isrngo  37898  rngoablo2  37910  rngoueqz  37941  isdivrngo  37951  isdrngo1  37957  isdrngo2  37959  ispridl2  38039  relcnveq3  38316  elrelscnveq3  38489  dmqsblocks  38852  ax12eq  38941  ax12el  38942  lkr0f  39094  hl2at  39406  dalemswapyz  39657  pclfinclN  39951  osumcllem11N  39967  pexmidlem8N  39978  ltrnnid  40137  aks4d1p8  42082  redvmptabs  42355  sn-00id  42396  rictr  42515  eu6w  42671  mptfcl  42715  fphpd  42811  elmnc  43132  itgoval  43157  arearect  43211  reabsifpos  43630  clsk3nimkb  44036  grumnud  44282  nanorxor  44301  pm11.71  44393  iotavalsb  44429  sbiota1  44430  2uasbanh  44558  eel0TT  44700  eelT00  44701  eelTTT  44702  eelT11  44703  eelT12  44705  eelTT1  44706  eelT01  44707  eel0T1  44708  eelTT  44767  uunT1p1  44777  uun121  44779  uun121p1  44780  un2122  44786  uunTT1  44789  uunTT1p1  44790  uunTT1p2  44791  uunT11  44792  uunT11p1  44793  uunT11p2  44794  uunT12  44795  uunT12p1  44796  uunT12p2  44797  uunT12p3  44798  uunT12p4  44799  uunT12p5  44800  uun111  44801  3anidm12p2  44803  uun123  44804  3impdirp1  44812  undif3VD  44878  ax6e2ndeqVD  44905  2uasbanhVD  44907  ax6e2ndeqALT  44927  iunconnlem2  44931  sineq0ALT  44933  modelaxreplem1  44975  permaxrep  45003  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem3  46008  stoweidlem17  46022  fourierdlem42  46154  fourierdlem48  46159  fourierdlem50  46161  fourierdlem51  46162  fourierdlem76  46187  fourierdlem83  46194  fourierdlem87  46198  hoidmvval0  46592  evenwodadd  46893  rexrsb  47105  2reu8i  47118  2reuimp  47120  afv0nbfvbi  47156  afvfv0bi  47157  afveu  47158  fnbrafvb  47159  afvres  47177  tz6.12-afv  47178  dmfcoafv  47180  afvco2  47181  aovprc  47193  aovrcl  47194  aovmpt4g  47206  afv2eu  47243  afv2res  47244  tz6.12-afv2  47245  tz6.12i-afv2  47248  afv2rnfveq  47267  fvmptrab  47297  fvmptrabdm  47298  fzopred  47327  2ffzoeq  47332  elsprel  47480  prproropf1o  47512  reupr  47527  lighneal  47616  odd2prm2  47723  even3prm2  47724  grictr  47927  grlimgrtrilem2  47998  usgrexmpl12ngric  48033  gpgprismgr4cycllem8  48096  gpgprismgr4cycllem11  48099  pgnbgreunbgrlem2lem1  48108  upgrwlkupwlk  48132  ovn0ssdmfun  48151  islinindfis  48442  rrx2linest  48735  line2ylem  48744  mofeu  48840  homf0  49002  uobffth  49211  uobeqw  49212  initopropd  49236  termopropd  49237  zeroopropd  49238  fucofvalne  49318  isthincd2  49430  lanrcl  49614  ranrcl  49615  setrec2fun  49685  elsetrecslem  49692  setrecsres  49695  secval  49740  cscval  49741  cotval  49742