Theorem sylbir 234

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3i  291  ex  414  3expa  1119  3ori  1425  nanass  1509  19.38  1842  19.35  1881  19.8aw  2054  equsexv  2260  sbi2  2299  nfeqf2  2377  equsex  2418  dfmoeu  2531  2mo  2645  axie2  2699  necon1bi  2970  necon1i  2975  r19.35  3109  r19.35OLD  3110  sbhypfOLD  3540  spc2ed  3592  reu6  3723  rabssrabd  4082  uneqin  4279  difin0ss  4369  inelcm  4465  rzal  4509  ralf0  4514  falseral0  4520  raaan2  4525  difprsn1  4804  tppreqb  4809  n0snor2el  4835  unissint  4977  intminss  4979  dfiun2g  5034  iununi  5103  triin  5283  bm1.3ii  5303  eusv2nf  5394  reusv3i  5403  moabex  5460  copsex2gOLD  5495  opelopabt  5533  eqrelrel  5798  opeliunxp2  5839  opelrn  5943  ssxpb  6174  xpima  6182  xpimasn  6185  dmsn0el  6211  relcnvtr  6267  relcoi2  6277  elsnxp  6291  reuop  6293  iotanul  6522  dffv2  6987  fnfvrnss  7120  fressnfv  7158  fconst5  7207  f1mpt  7260  isocnv3  7329  f1owe  7350  ovprc  7447  fvmpopr2d  7569  onminesb  7781  onminsb  7782  onintrab  7784  onnminsb  7787  ordsuci  7796  onsucuni2  7822  tfindsg2  7851  zfrep6  7941  fo1stres  8001  fo2ndres  8002  bropopvvv  8076  bropfvvvv  8078  frxp  8112  poseq  8144  soseq  8145  opeliunxp2f  8195  mpoxopoveqd  8206  reldmtpos  8219  frrlem4  8274  wfrlem4OLD  8312  wfrlem12OLD  8320  wfrlem16OLD  8324  wfr2OLD  8328  tfrlem5  8380  tfrlem9  8385  tfr2  8398  rdgsuc  8424  oaordi  8546  oeordi  8587  omopthi  8660  on2recsov  8667  fvmptmap  8875  mptelixpg  8929  ener  8997  domtr  9003  snfi  9044  unen  9046  undom  9059  dom0  9102  xpf1o  9139  mapen  9141  rexdif1enOLD  9159  dif1enOLD  9162  pssnn  9168  unfi  9172  ssfi  9173  ensymfib  9187  entrfil  9188  enfii  9189  domtrfil  9195  unxpdomlem3  9252  isinf  9260  isinfOLD  9261  frfi  9288  unblem1  9295  unfiOLD  9313  fofinf1o  9327  fsuppun  9382  inf3lem2  9624  inf3lem5  9627  cantnfp1lem1  9673  cantnfp1lem3  9675  tcmin  9736  frr2  9755  r1ordg  9773  r1ord  9775  rankr1ai  9793  r1val3  9833  bndrank  9836  unbndrank  9837  rankr1b  9859  rankxplim3  9876  tcrank  9879  xpnum  9946  cardmin2  9994  infxpenlem  10008  fseqen  10022  dfac8clem  10027  alephsson  10095  alephfp  10103  dfac4  10117  kmlem6  10150  kmlem8  10152  kmlem9  10153  infpssr  10303  fin1a2lem12  10406  axcc4  10434  axcc4dom  10436  ac6s2  10481  zornn0g  10500  cardidg  10543  unsnen  10548  pwcfsdom  10578  cfpwsdom  10579  gchpwdom  10665  r1tskina  10777  intgru  10809  indpi  10902  nqereu  10924  supsrlem  11106  letrii  11339  dfnn3  12226  zaddcl  12602  nn0ind  12657  fnn0ind  12661  ublbneg  12917  nn01to3  12925  infmrp1  13323  fz0  13516  fzo1fzo0n0  13683  elfzom1elp1fzo  13699  fzo0end  13724  elfznelfzo  13737  fzind2  13750  injresinjlem  13752  fleqceilz  13819  nnsinds  13953  nn0sinds  13954  faclbnd4lem1  14253  hashinf  14295  hasheqf1oi  14311  hashgt0elex  14361  hashgt23el  14384  hashfacen  14413  hashfacenOLD  14414  hash2prde  14431  hash2sspr  14449  fun2dmnop0  14455  iswrddm0  14488  swrdnnn0nd  14606  swrdnd0  14607  swrdlsw  14617  pfxn0  14636  pfxnd0  14638  swrdswrdlem  14654  pfxccatin12lem3  14682  pfxccat3  14684  pfxccat3a  14688  swrdccat3blem  14689  cshwsublen  14746  cshwidxmod  14753  repswcshw  14762  cshw1  14772  trclun  14961  dmtrclfv  14965  rediv  15078  imdiv  15085  fsump1i  15715  modfsummods  15739  bpolydiflem  15998  bpoly3  16002  bpoly4  16003  cos1bnd  16130  sinltx  16132  rpnnen2lem1  16157  rpnnen2lem2  16158  rpnnen2lem12  16168  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  gcdcllem1  16440  gcdaddmlem  16465  dfgcd2  16488  algfx  16517  lcmledvds  16536  lcmfunsnlem  16578  lcmfun  16582  coprmprod  16598  coprmproddvdslem  16599  odzval  16724  odzdvds  16728  prmreclem5  16853  mul4sq  16887  prmgaplem5  16988  prmgaplem6  16989  imasaddfnlem  17474  mreexexlem4d  17591  joindmss  18332  meetdmss  18346  gictr  19149  cntzval  19185  symg2bas  19260  odfval  19400  efgsfo  19607  efgrelexlemb  19618  dprddomcld  19871  dprdsubg  19894  dprd2da  19912  lssacs  20578  cnfldinv  20976  ocvval  21220  selvval  21681  dmatmul  21999  mdetfval1  22092  mndifsplit  22138  fvmptnn04if  22351  toprntopon  22427  opnnei  22624  ordtbas2  22695  ordtrest2lem  22707  lmmo  22884  fincmp  22897  bwth  22914  txbas  23071  ptcnplem  23125  tx2ndc  23155  hmphtr  23287  fbun  23344  filconn  23387  ptcmplem5  23560  cnextcn  23571  utoptop  23739  ucncn  23790  metust  24067  cfilucfil  24068  elcncf1di  24411  xrhmeo  24462  phtpycc  24507  copco  24534  pcohtpylem  24535  pcopt  24538  pcopt2  24539  ncvsi  24668  ovolval  24990  iunmbl2  25074  itg2splitlem  25266  cpnfval  25449  plyval  25707  fta1  25821  aaliou2b  25854  tayl0  25874  ulmdvlem3  25914  radcnvlem2  25926  dvradcnv  25933  reeff1o  25959  sincosq1lem  26007  sincosq2sgn  26009  sincosq4sgn  26011  sinq12ge0  26018  logrncl  26076  eflog  26085  cxpge0  26191  logb1  26274  atanf  26385  atanbnd  26431  igamf  26555  igamcl  26556  lgsne0  26838  mul2sq  26922  2sqreultblem  26951  pntibnd  27096  ostth  27142  nocvxminlem  27279  nocvxmin  27280  cutlt  27419  norec2ov  27441  addsuniflem  27484  mulsuniflem  27604  mptelee  28153  axlowdimlem9  28208  axlowdimlem12  28211  axcontlem2  28223  axcontlem12  28233  structgrssvtx  28284  structgrssiedg  28285  lpvtx  28328  nbuhgr  28600  nbumgr  28604  nbuhgr2vtx1edgblem  28608  nbgr0vtxlem  28612  nbgr1vtx  28615  uvtx01vtx  28654  prcliscplgr  28671  cusgrsizeinds  28709  sizusglecusglem2  28719  uhgrvd00  28791  fusgrregdegfi  28826  rusgr1vtxlem  28844  wlkeq  28891  wlk1walk  28896  uspgr2wlkeq  28903  wlklenvclwlk  28912  wlkreslem  28926  wlkdlem2  28940  wlkdlem4  28942  spthonepeq  29009  clwlkclwwlkflem  29257  clwlkclwwlkfolem  29260  clwlkclwwlkf  29261  clwwisshclwws  29268  clwwlkneq0  29282  3wlkdlem6  29418  eupth2eucrct  29470  eupth2lem1  29471  eupth2lem3lem7  29487  frgr3vlem1  29526  frgr3vlem2  29527  frgrncvvdeqlem8  29559  frgrncvvdeqlem9  29560  numclwwlk5  29641  frgrreg  29647  frgrregord013  29648  friendshipgt3  29651  isgrpo  29750  vciOLD  29814  vcex  29831  nmogtmnf  30023  siilem1  30104  siii  30106  ajmoi  30111  bcsiALT  30432  hhcms  30456  ocval  30533  hsupval  30587  omlsilem  30655  h1de2bi  30807  h1de2ctlem  30808  hosubeq0i  31079  adjmo  31085  nmopgtmnf  31121  nlfnval  31134  nmcopex  31282  nmcfnex  31306  riesz4i  31316  riesz1  31318  riesz2  31319  opsqrlem1  31393  superpos  31607  hatomistici  31615  chpssati  31616  mdsymlem3  31658  3o1cs  31703  3o2cs  31704  3o3cs  31705  iunrnmptss  31797  brabgaf  31837  f1mptrn  31859  ffsrn  31954  fpwrelmap  31958  xnn0gt0  31982  hashxpe  32019  prmidl2  32559  mxidlnzrb  32595  fedgmul  32716  ordtrest2NEWlem  32902  qqhval2  32962  esumfsup  33068  esumcvg  33084  cntnevol  33226  ddemeas  33234  dya2icoseg2  33277  dya2iocnei  33281  eulerpartlems  33359  eulerpartlemgvv  33375  eulerpart  33381  cndprobprob  33437  ballotlemsdom  33510  ballotth  33536  sgn3da  33540  bnj945  33784  bnj1379  33841  bnj1459  33854  bnj557  33912  bnj571  33917  bnj849  33936  bnj964  33954  bnj978  33960  bnj1018g  33974  bnj1018  33975  bnj1020  33976  bnj1033  33980  bnj1175  34015  bnj1398  34045  bnj1417  34052  bnj1523  34082  nummin  34094  cusgr3cyclex  34127  txpconn  34223  satfv1  34354  satffun  34400  msubco  34522  mclsax  34560  setinds  34750  dfon2lem7  34761  dfon2lem8  34762  pprodss4v  34856  fullfunfv  34919  altxpsspw  34949  funtransport  35003  fvtransport  35004  funray  35112  fvray  35113  funline  35114  fvline  35116  finminlem  35203  bisym1  35304  onsucconni  35322  onsucsuccmpi  35328  bj-currypara  35436  axc11n11r  35561  bj-equsal2  35703  bj-xpima1snALT  35838  bj-unexg  35919  bj-bm1.3ii  35945  bj-opelidb1ALT  36047  mptsnunlem  36219  iooelexlt  36243  relowlpssretop  36245  rdgeqoa  36251  difunieq  36255  nlpineqsn  36289  fvineqsneq  36293  wl-lem-nexmo  36432  matunitlindflem1  36484  ptrecube  36488  poimirlem26  36514  poimirlem30  36518  poimir  36521  ismblfin  36529  itg2addnclem  36539  dvasin  36572  sdclem2  36610  totbndbnd  36657  ismgmOLD  36718  exidresid  36747  isrngo  36765  rngoablo2  36777  rngoueqz  36808  isdivrngo  36818  isdrngo1  36824  isdrngo2  36826  ispridl2  36906  relcnveq3  37190  elrelscnveq3  37361  ax12eq  37811  ax12el  37812  lkr0f  37964  hl2at  38276  dalemswapyz  38527  pclfinclN  38821  osumcllem11N  38837  pexmidlem8N  38848  ltrnnid  39007  aks4d1p8  40952  rictr  41095  sn-00id  41274  mptfcl  41458  fphpd  41554  elmnc  41878  itgoval  41903  arearect  41964  reabsifpos  42385  clsk3nimkb  42791  grumnud  43045  nanorxor  43064  pm11.71  43156  iotavalsb  43192  sbiota1  43193  2uasbanh  43322  eel0TT  43465  eelT00  43466  eelTTT  43467  eelT11  43468  eelT12  43470  eelTT1  43471  eelT01  43472  eel0T1  43473  eelTT  43532  uunT1p1  43542  uun121  43544  uun121p1  43545  un2122  43551  uunTT1  43554  uunTT1p1  43555  uunTT1p2  43556  uunT11  43557  uunT11p1  43558  uunT11p2  43559  uunT12  43560  uunT12p1  43561  uunT12p2  43562  uunT12p3  43563  uunT12p4  43564  uunT12p5  43565  uun111  43566  3anidm12p2  43568  uun123  43569  3impdirp1  43577  undif3VD  43643  ax6e2ndeqVD  43670  2uasbanhVD  43672  ax6e2ndeqALT  43692  iunconnlem2  43696  sineq0ALT  43698  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem3  44719  stoweidlem17  44733  fourierdlem42  44865  fourierdlem48  44870  fourierdlem50  44872  fourierdlem51  44873  fourierdlem76  44898  fourierdlem83  44905  fourierdlem87  44909  hoidmvval0  45303  rexrsb  45808  2reu8i  45821  2reuimp  45823  afv0nbfvbi  45859  afvfv0bi  45860  afveu  45861  fnbrafvb  45862  afvres  45880  tz6.12-afv  45881  dmfcoafv  45883  afvco2  45884  aovprc  45896  aovrcl  45897  aovmpt4g  45909  afv2eu  45946  afv2res  45947  tz6.12-afv2  45948  tz6.12i-afv2  45951  afv2rnfveq  45970  fvmptrab  46000  fvmptrabdm  46001  fzopred  46030  2ffzoeq  46036  elsprel  46143  prproropf1o  46175  reupr  46190  lighneal  46279  odd2prm2  46386  even3prm2  46387  upgrwlkupwlk  46518  ovn0ssdmfun  46537  pzriprnglem7  46811  islinindfis  47130  rrx2linest  47428  line2ylem  47437  mofeu  47514  isthincd2  47658  setrec2fun  47737  elsetrecslem  47744  setrecsres  47747  secval  47792  cscval  47793  cotval  47794