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  an42ds  1491  nanass  1511  19.38  1840  19.35  1878  19.8aw  2053  equsexv  2273  sbi2  2306  nfeqf2  2379  equsex  2420  dfmoeu  2533  2mo  2646  axie2  2701  necon1bi  2958  necon1i  2963  r19.35  3092  spc2ed  3553  reu6  3682  rabssrabd  4033  uneqin  4239  difin0ss  4323  inelcm  4415  falseral0OLD  4466  raaan2  4473  difprsn1  4754  tppreqb  4759  n0snor2el  4787  unissint  4925  intminss  4927  dfiun2g  4983  iununi  5052  triin  5219  bm1.3iiOLD  5245  eusv2nf  5338  reusv3i  5347  moabexOLD  5405  opelopabt  5478  eqrelrel  5744  opeliunxp2  5785  opelrn  5890  ssxpb  6130  xpima  6138  xpimasn  6141  dmsn0el  6167  relcnvtr  6224  relcoi2  6233  elsnxp  6247  reuop  6249  iotanul  6470  f1imadifssran  6576  dffv2  6927  fnfvrnss  7064  fressnfv  7103  fconst5  7150  f1mpt  7205  isocnv3  7276  f1owe  7297  ovprc  7394  fvmpopr2d  7518  onminesb  7736  onminsb  7737  onintrab  7739  onnminsb  7742  ordsuci  7751  onsucuni2  7774  tfindsg2  7802  zfrep6  7897  fo1stres  7957  fo2ndres  7958  bropopvvv  8030  bropfvvvv  8032  frxp  8066  poseq  8098  soseq  8099  opeliunxp2f  8150  mpoxopoveqd  8161  reldmtpos  8174  frrlem4  8229  tfrlem5  8309  tfrlem9  8314  tfr2  8327  rdgsuc  8353  oaordi  8471  oeordi  8513  omopthi  8587  on2recsov  8594  fvmptmap  8817  mptelixpg  8871  ener  8936  domtr  8942  unen  8980  undom  8991  dom0  9031  xpf1o  9065  mapen  9067  pssnn  9091  unfi  9093  ssfi  9095  ensymfib  9106  entrfil  9107  enfii  9108  domtrfil  9114  unxpdomlem3  9156  isinf  9163  frfi  9183  unblem1  9190  fofinf1o  9230  fsuppun  9288  elirrv  9500  inf3lem2  9536  inf3lem5  9539  cantnfp1lem1  9585  cantnfp1lem3  9587  tcmin  9646  setinds  9656  frr2  9670  r1ordg  9688  r1ord  9690  rankr1ai  9708  r1val3  9748  bndrank  9751  unbndrank  9752  rankr1b  9774  rankxplim3  9791  tcrank  9794  xpnum  9861  cardmin2  9909  infxpenlem  9921  fseqen  9935  dfac8clem  9940  alephsson  10008  alephfp  10016  dfac4  10030  kmlem6  10064  kmlem8  10066  kmlem9  10067  cflem  10153  infpssr  10216  fin1a2lem12  10319  axcc4  10347  axcc4dom  10349  ac6s2  10394  zornn0g  10413  cardidg  10456  unsnen  10461  pwcfsdom  10492  cfpwsdom  10493  gchpwdom  10579  r1tskina  10691  intgru  10723  indpi  10816  nqereu  10838  supsrlem  11020  letrii  11256  dfnn3  12157  zaddcl  12529  nn0ind  12585  fnn0ind  12589  ublbneg  12844  nn01to3  12852  infmrp1  13258  fz0  13453  fzo1fzo0n0  13629  elfzom1elp1fzo  13646  fzo0end  13672  elfznelfzo  13687  fzind2  13702  injresinjlem  13704  fleqceilz  13772  nnsinds  13909  nn0sinds  13910  faclbnd4lem1  14214  hashinf  14256  hasheqf1oi  14272  hashgt0elex  14322  hashgt23el  14345  hashfacen  14375  hash2prde  14391  hash2sspr  14410  fun2dmnop0  14425  iswrddm0  14459  swrdnnn0nd  14578  swrdnd0  14579  swrdlsw  14589  pfxn0  14608  pfxnd0  14610  swrdswrdlem  14625  pfxccatin12lem3  14653  pfxccat3  14655  pfxccat3a  14659  swrdccat3blem  14660  cshwsublen  14717  cshwidxmod  14724  repswcshw  14733  cshw1  14743  trclun  14935  dmtrclfv  14939  rediv  15052  imdiv  15059  fsump1i  15690  modfsummods  15714  bpolydiflem  15975  bpoly3  15979  bpoly4  15980  cos1bnd  16110  sinltx  16112  rpnnen2lem1  16137  rpnnen2lem2  16138  rpnnen2lem12  16148  odd2np1  16266  opoe  16288  omoe  16289  opeo  16290  omeo  16291  gcdcllem1  16424  gcdaddmlem  16449  dfgcd2  16471  algfx  16505  lcmledvds  16524  lcmfunsnlem  16566  lcmfun  16570  coprmprod  16586  coprmproddvdslem  16587  odzval  16717  odzdvds  16721  prmreclem5  16846  mul4sq  16880  prmgaplem5  16981  prmgaplem6  16982  imasaddfnlem  17447  mreexexlem4d  17568  joindmss  18298  meetdmss  18312  gictr  19203  cntzval  19248  symg2bas  19320  odfval  19459  efgsfo  19666  efgrelexlemb  19677  dprddomcld  19930  dprdsubg  19953  dprd2da  19971  lssacs  20916  cnfldinv  21355  pzriprnglem7  21440  ocvval  21620  selvval  22076  dmatmul  22439  mdetfval1  22532  mndifsplit  22578  fvmptnn04if  22791  toprntopon  22867  opnnei  23062  ordtbas2  23133  ordtrest2lem  23145  lmmo  23322  fincmp  23335  bwth  23352  txbas  23509  ptcnplem  23563  tx2ndc  23593  hmphtr  23725  fbun  23782  filconn  23825  ptcmplem5  23998  cnextcn  24009  utoptop  24176  ucncn  24226  metust  24500  cfilucfil  24501  elcncf1di  24842  xrhmeo  24898  phtpycc  24944  copco  24972  pcohtpylem  24973  pcopt  24976  pcopt2  24977  ncvsi  25105  ovolval  25428  iunmbl2  25512  itg2splitlem  25703  cpnfval  25888  plyval  26152  fta1  26270  aaliou2b  26303  tayl0  26323  ulmdvlem3  26365  radcnvlem2  26377  dvradcnv  26384  reeff1o  26411  sincosq1lem  26460  sincosq2sgn  26462  sincosq4sgn  26464  sinq12ge0  26471  logrncl  26530  eflog  26539  cxpge0  26646  logb1  26733  atanf  26844  atanbnd  26890  igamf  27015  igamcl  27016  lgsne0  27300  mul2sq  27384  2sqreultblem  27413  pntibnd  27558  ostth  27604  nobdaymin  27743  nocvxminlem  27744  cutlt  27903  norec2ov  27927  addsuniflem  27971  mulsuniflem  28118  oldfib  28335  zmulscld  28355  zseo  28380  zs12addscl  28426  mpteleeOLD  28917  axlowdimlem9  28972  axlowdimlem12  28975  axcontlem2  28987  axcontlem12  28997  structgrssvtx  29046  structgrssiedg  29047  lpvtx  29090  nbuhgr  29365  nbumgr  29369  nbuhgr2vtx1edgblem  29373  nbgr0edglem  29378  nbgr1vtx  29380  uvtx01vtx  29419  prcliscplgr  29436  cusgrsizeinds  29475  sizusglecusglem2  29485  uhgrvd00  29557  fusgrregdegfi  29592  rusgr1vtxlem  29610  wlkeq  29656  wlk1walk  29661  uspgr2wlkeq  29668  wlklenvclwlk  29676  wlkreslem  29690  wlkdlem2  29704  wlkdlem4  29706  spthonepeq  29774  cyclnumvtx  29822  clwlkclwwlkflem  30028  clwlkclwwlkfolem  30031  clwlkclwwlkf  30032  clwwisshclwws  30039  clwwlkneq0  30053  3wlkdlem6  30189  eupth2eucrct  30241  eupth2lem1  30242  eupth2lem3lem7  30258  frgr3vlem1  30297  frgr3vlem2  30298  frgrncvvdeqlem8  30330  frgrncvvdeqlem9  30331  numclwwlk5  30412  frgrreg  30418  frgrregord013  30419  friendshipgt3  30422  isgrpo  30521  vciOLD  30585  vcex  30602  nmogtmnf  30794  siilem1  30875  siii  30877  ajmoi  30882  bcsiALT  31203  hhcms  31227  ocval  31304  hsupval  31358  omlsilem  31426  h1de2bi  31578  h1de2ctlem  31579  hosubeq0i  31850  adjmo  31856  nmopgtmnf  31892  nlfnval  31905  nmcopex  32053  nmcfnex  32077  riesz4i  32087  riesz1  32089  riesz2  32090  opsqrlem1  32164  superpos  32378  hatomistici  32386  chpssati  32387  mdsymlem3  32429  3o1cs  32484  3o2cs  32485  3o3cs  32486  iunrnmptss  32589  brabgaf  32633  f1mptrn  32662  ffsrn  32756  xnn0gt0  32798  hashxpe  32836  sgn3da  32864  elrgspnlem4  33276  prmidl2  33471  mxidlnzrb  33510  evl1deg2  33607  evl1deg3  33608  fedgmul  33737  cos9thpiminplylem2  33889  ordtrest2NEWlem  34028  qqhval2  34088  esumfsup  34176  esumcvg  34192  cntnevol  34334  ddemeas  34342  dya2icoseg2  34384  dya2iocnei  34388  eulerpartlems  34466  eulerpartlemgvv  34482  eulerpart  34488  cndprobprob  34544  ballotlemsdom  34618  ballotth  34644  bnj945  34878  bnj1379  34935  bnj1459  34948  bnj557  35006  bnj571  35011  bnj849  35030  bnj964  35048  bnj978  35054  bnj1018g  35068  bnj1018  35069  bnj1020  35070  bnj1033  35074  bnj1175  35109  bnj1398  35139  bnj1417  35146  bnj1523  35176  nummin  35198  r1omhf  35211  fineqvnttrclselem1  35226  onvf1odlem4  35249  onvf1od  35250  cusgr3cyclex  35279  txpconn  35375  satfv1  35506  satffun  35552  msubco  35674  mclsax  35712  dfon2lem7  35930  dfon2lem8  35931  pprodss4v  36025  fullfunfv  36090  altxpsspw  36120  funtransport  36174  fvtransport  36175  funray  36283  fvray  36284  funline  36285  fvline  36287  finminlem  36461  bisym1  36562  onsucconni  36580  onsucsuccmpi  36586  weiunse  36611  bj-currypara  36703  axc11n11r  36827  bj-equsal2  36969  bj-xpima1snALT  37101  bj-unexg  37182  bj-bm1.3ii  37208  bj-opelidb1ALT  37310  mptsnunlem  37482  iooelexlt  37506  relowlpssretop  37508  rdgeqoa  37514  difunieq  37518  nlpineqsn  37552  fvineqsneq  37556  wl-ax12v2cl  37650  wl-lem-nexmo  37711  matunitlindflem1  37756  ptrecube  37760  poimirlem26  37786  poimirlem30  37790  poimir  37793  ismblfin  37801  itg2addnclem  37811  dvasin  37844  sdclem2  37882  totbndbnd  37929  ismgmOLD  37990  exidresid  38019  isrngo  38037  rngoablo2  38049  rngoueqz  38080  isdivrngo  38090  isdrngo1  38096  isdrngo2  38098  ispridl2  38178  relcnveq3  38459  elrelscnveq3  38739  dmqsblocks  39051  ax12eq  39140  ax12el  39141  lkr0f  39293  hl2at  39604  dalemswapyz  39855  pclfinclN  40149  osumcllem11N  40165  pexmidlem8N  40176  ltrnnid  40335  aks4d1p8  42280  redvmptabs  42557  sn-00id  42598  rictr  42717  eu6w  42861  mptfcl  42904  fphpd  43000  elmnc  43320  itgoval  43345  arearect  43399  reabsifpos  43817  clsk3nimkb  44223  grumnud  44469  nanorxor  44488  pm11.71  44580  iotavalsb  44616  sbiota1  44617  2uasbanh  44744  eel0TT  44886  eelT00  44887  eelTTT  44888  eelT11  44889  eelT12  44891  eelTT1  44892  eelT01  44893  eel0T1  44894  eelTT  44953  uunT1p1  44963  uun121  44965  uun121p1  44966  un2122  44972  uunTT1  44975  uunTT1p1  44976  uunTT1p2  44977  uunT11  44978  uunT11p1  44979  uunT11p2  44980  uunT12  44981  uunT12p1  44982  uunT12p2  44983  uunT12p3  44984  uunT12p4  44985  uunT12p5  44986  uun111  44987  3anidm12p2  44989  uun123  44990  3impdirp1  44998  undif3VD  45064  ax6e2ndeqVD  45091  2uasbanhVD  45093  ax6e2ndeqALT  45113  iunconnlem2  45117  sineq0ALT  45119  modelaxreplem1  45161  permaxrep  45189  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  stoweidlem3  46189  stoweidlem17  46203  fourierdlem42  46335  fourierdlem48  46340  fourierdlem50  46342  fourierdlem51  46343  fourierdlem76  46368  fourierdlem83  46375  fourierdlem87  46379  hoidmvval0  46773  evenwodadd  47073  rexrsb  47288  2reu8i  47301  2reuimp  47303  afv0nbfvbi  47339  afvfv0bi  47340  afveu  47341  fnbrafvb  47342  afvres  47360  tz6.12-afv  47361  dmfcoafv  47363  afvco2  47364  aovprc  47376  aovrcl  47377  aovmpt4g  47389  afv2eu  47426  afv2res  47427  tz6.12-afv2  47428  tz6.12i-afv2  47431  afv2rnfveq  47450  fvmptrab  47480  fvmptrabdm  47481  fzopred  47510  2ffzoeq  47515  elsprel  47663  prproropf1o  47695  reupr  47710  lighneal  47799  odd2prm2  47906  even3prm2  47907  grictr  48111  grlimgrtrilem2  48190  usgrexmpl12ngric  48226  gpgprismgr4cycllem8  48290  gpgprismgr4cycllem11  48293  pgnbgreunbgrlem2lem1  48302  upgrwlkupwlk  48328  ovn0ssdmfun  48347  islinindfis  48637  rrx2linest  48930  line2ylem  48939  mofeu  49035  homf0  49196  uobffth  49405  uobeqw  49406  initopropd  49430  termopropd  49431  zeroopropd  49432  fucofvalne  49512  isthincd2  49624  lanrcl  49808  ranrcl  49809  setrec2fun  49879  elsetrecslem  49886  setrecsres  49889  secval  49934  cscval  49935  cotval  49936