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  1117  3ori  1423  nanass  1506  19.38  1835  19.35  1874  19.8aw  2047  equsexv  2265  sbi2  2300  nfeqf2  2379  equsex  2420  dfmoeu  2533  2mo  2645  axie2  2700  necon1bi  2966  necon1i  2971  r19.35  3105  r19.35OLD  3106  sbhypfOLD  3544  spc2ed  3600  reu6  3734  rabssrabd  4092  uneqin  4294  difin0ss  4378  inelcm  4470  rzal  4514  ralf0  4519  falseral0  4521  raaan2  4526  difprsn1  4804  tppreqb  4809  n0snor2el  4837  unissint  4976  intminss  4978  dfiun2g  5034  iununi  5103  triin  5281  bm1.3iiOLD  5307  eusv2nf  5400  reusv3i  5409  moabex  5469  opelopabt  5541  eqrelrel  5809  opeliunxp2  5851  opelrn  5956  ssxpb  6195  xpima  6203  xpimasn  6206  dmsn0el  6232  relcnvtr  6288  relcoi2  6298  elsnxp  6312  reuop  6314  iotanul  6540  dffv2  7003  fnfvrnss  7140  fressnfv  7179  fconst5  7225  f1mpt  7280  isocnv3  7351  f1owe  7372  ovprc  7468  fvmpopr2d  7594  onminesb  7812  onminsb  7813  onintrab  7815  onnminsb  7818  ordsuci  7827  onsucuni2  7853  tfindsg2  7882  zfrep6  7977  fo1stres  8038  fo2ndres  8039  bropopvvv  8113  bropfvvvv  8115  frxp  8149  poseq  8181  soseq  8182  opeliunxp2f  8233  mpoxopoveqd  8244  reldmtpos  8257  frrlem4  8312  wfrlem4OLD  8350  wfrlem12OLD  8358  wfrlem16OLD  8362  wfr2OLD  8366  tfrlem5  8418  tfrlem9  8423  tfr2  8436  rdgsuc  8462  oaordi  8582  oeordi  8623  omopthi  8697  on2recsov  8704  fvmptmap  8919  mptelixpg  8973  ener  9039  domtr  9045  snfiOLD  9082  unen  9084  undom  9097  dom0  9140  xpf1o  9177  mapen  9179  rexdif1enOLD  9197  dif1enOLD  9200  pssnn  9206  unfi  9209  ssfi  9211  ensymfib  9221  entrfil  9222  enfii  9223  domtrfil  9229  unxpdomlem3  9285  isinf  9293  isinfOLD  9294  frfi  9318  unblem1  9325  fofinf1o  9369  fsuppun  9424  inf3lem2  9666  inf3lem5  9669  cantnfp1lem1  9715  cantnfp1lem3  9717  tcmin  9778  frr2  9797  r1ordg  9815  r1ord  9817  rankr1ai  9835  r1val3  9875  bndrank  9878  unbndrank  9879  rankr1b  9901  rankxplim3  9918  tcrank  9921  xpnum  9988  cardmin2  10036  infxpenlem  10050  fseqen  10064  dfac8clem  10069  alephsson  10137  alephfp  10145  dfac4  10159  kmlem6  10193  kmlem8  10195  kmlem9  10196  cflem  10282  infpssr  10345  fin1a2lem12  10448  axcc4  10476  axcc4dom  10478  ac6s2  10523  zornn0g  10542  cardidg  10585  unsnen  10590  pwcfsdom  10620  cfpwsdom  10621  gchpwdom  10707  r1tskina  10819  intgru  10851  indpi  10944  nqereu  10966  supsrlem  11148  letrii  11383  dfnn3  12277  zaddcl  12654  nn0ind  12710  fnn0ind  12714  ublbneg  12972  nn01to3  12980  infmrp1  13382  fz0  13575  fzo1fzo0n0  13750  elfzom1elp1fzo  13767  fzo0end  13793  elfznelfzo  13807  fzind2  13820  injresinjlem  13822  fleqceilz  13890  nnsinds  14025  nn0sinds  14026  faclbnd4lem1  14328  hashinf  14370  hasheqf1oi  14386  hashgt0elex  14436  hashgt23el  14459  hashfacen  14489  hash2prde  14505  hash2sspr  14524  fun2dmnop0  14539  iswrddm0  14572  swrdnnn0nd  14690  swrdnd0  14691  swrdlsw  14701  pfxn0  14720  pfxnd0  14722  swrdswrdlem  14738  pfxccatin12lem3  14766  pfxccat3  14768  pfxccat3a  14772  swrdccat3blem  14773  cshwsublen  14830  cshwidxmod  14837  repswcshw  14846  cshw1  14856  trclun  15049  dmtrclfv  15053  rediv  15166  imdiv  15173  fsump1i  15801  modfsummods  15825  bpolydiflem  16086  bpoly3  16090  bpoly4  16091  cos1bnd  16219  sinltx  16221  rpnnen2lem1  16246  rpnnen2lem2  16247  rpnnen2lem12  16257  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  gcdcllem1  16532  gcdaddmlem  16557  dfgcd2  16579  algfx  16613  lcmledvds  16632  lcmfunsnlem  16674  lcmfun  16678  coprmprod  16694  coprmproddvdslem  16695  odzval  16824  odzdvds  16828  prmreclem5  16953  mul4sq  16987  prmgaplem5  17088  prmgaplem6  17089  imasaddfnlem  17574  mreexexlem4d  17691  joindmss  18436  meetdmss  18450  gictr  19306  cntzval  19351  symg2bas  19424  odfval  19564  efgsfo  19771  efgrelexlemb  19782  dprddomcld  20035  dprdsubg  20058  dprd2da  20076  lssacs  20982  cnfldinv  21432  pzriprnglem7  21515  ocvval  21702  selvval  22156  dmatmul  22518  mdetfval1  22611  mndifsplit  22657  fvmptnn04if  22870  toprntopon  22946  opnnei  23143  ordtbas2  23214  ordtrest2lem  23226  lmmo  23403  fincmp  23416  bwth  23433  txbas  23590  ptcnplem  23644  tx2ndc  23674  hmphtr  23806  fbun  23863  filconn  23906  ptcmplem5  24079  cnextcn  24090  utoptop  24258  ucncn  24309  metust  24586  cfilucfil  24587  elcncf1di  24934  xrhmeo  24990  phtpycc  25036  copco  25064  pcohtpylem  25065  pcopt  25068  pcopt2  25069  ncvsi  25198  ovolval  25521  iunmbl2  25605  itg2splitlem  25797  cpnfval  25982  plyval  26246  fta1  26364  aaliou2b  26397  tayl0  26417  ulmdvlem3  26459  radcnvlem2  26471  dvradcnv  26478  reeff1o  26505  sincosq1lem  26553  sincosq2sgn  26555  sincosq4sgn  26557  sinq12ge0  26564  logrncl  26623  eflog  26632  cxpge0  26739  logb1  26826  atanf  26937  atanbnd  26983  igamf  27108  igamcl  27109  lgsne0  27393  mul2sq  27477  2sqreultblem  27506  pntibnd  27651  ostth  27697  nocvxminlem  27836  nocvxmin  27837  cutlt  27980  norec2ov  28004  addsuniflem  28048  mulsuniflem  28189  zmulscld  28397  zseo  28420  mptelee  28924  axlowdimlem9  28979  axlowdimlem12  28982  axcontlem2  28994  axcontlem12  29004  structgrssvtx  29055  structgrssiedg  29056  lpvtx  29099  nbuhgr  29374  nbumgr  29378  nbuhgr2vtx1edgblem  29382  nbgr0edglem  29387  nbgr1vtx  29389  uvtx01vtx  29428  prcliscplgr  29445  cusgrsizeinds  29484  sizusglecusglem2  29494  uhgrvd00  29566  fusgrregdegfi  29601  rusgr1vtxlem  29619  wlkeq  29666  wlk1walk  29671  uspgr2wlkeq  29678  wlklenvclwlk  29687  wlkreslem  29701  wlkdlem2  29715  wlkdlem4  29717  spthonepeq  29784  clwlkclwwlkflem  30032  clwlkclwwlkfolem  30035  clwlkclwwlkf  30036  clwwisshclwws  30043  clwwlkneq0  30057  3wlkdlem6  30193  eupth2eucrct  30245  eupth2lem1  30246  eupth2lem3lem7  30262  frgr3vlem1  30301  frgr3vlem2  30302  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  numclwwlk5  30416  frgrreg  30422  frgrregord013  30423  friendshipgt3  30426  isgrpo  30525  vciOLD  30589  vcex  30606  nmogtmnf  30798  siilem1  30879  siii  30881  ajmoi  30886  bcsiALT  31207  hhcms  31231  ocval  31308  hsupval  31362  omlsilem  31430  h1de2bi  31582  h1de2ctlem  31583  hosubeq0i  31854  adjmo  31860  nmopgtmnf  31896  nlfnval  31909  nmcopex  32057  nmcfnex  32081  riesz4i  32091  riesz1  32093  riesz2  32094  opsqrlem1  32168  superpos  32382  hatomistici  32390  chpssati  32391  mdsymlem3  32433  an42ds  32478  3o1cs  32489  3o2cs  32490  3o3cs  32491  iunrnmptss  32585  brabgaf  32627  f1mptrn  32651  ffsrn  32746  fpwrelmap  32750  xnn0gt0  32779  hashxpe  32816  elrgspnlem4  33234  prmidl2  33448  mxidlnzrb  33487  evl1deg2  33581  evl1deg3  33582  fedgmul  33658  ordtrest2NEWlem  33882  qqhval2  33944  esumfsup  34050  esumcvg  34066  cntnevol  34208  ddemeas  34216  dya2icoseg2  34259  dya2iocnei  34263  eulerpartlems  34341  eulerpartlemgvv  34357  eulerpart  34363  cndprobprob  34419  ballotlemsdom  34492  ballotth  34518  sgn3da  34522  bnj945  34765  bnj1379  34822  bnj1459  34835  bnj557  34893  bnj571  34898  bnj849  34917  bnj964  34935  bnj978  34941  bnj1018g  34955  bnj1018  34956  bnj1020  34957  bnj1033  34961  bnj1175  34996  bnj1398  35026  bnj1417  35033  bnj1523  35063  nummin  35083  cusgr3cyclex  35120  txpconn  35216  satfv1  35347  satffun  35393  msubco  35515  mclsax  35553  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  36300  bisym1  36401  onsucconni  36419  onsucsuccmpi  36425  weiunse  36450  bj-currypara  36542  axc11n11r  36665  bj-equsal2  36807  bj-xpima1snALT  36939  bj-unexg  37020  bj-bm1.3ii  37046  bj-opelidb1ALT  37148  mptsnunlem  37320  iooelexlt  37344  relowlpssretop  37346  rdgeqoa  37352  difunieq  37356  nlpineqsn  37390  fvineqsneq  37394  wl-ax12v2cl  37486  wl-lem-nexmo  37547  matunitlindflem1  37602  ptrecube  37606  poimirlem26  37632  poimirlem30  37636  poimir  37639  ismblfin  37647  itg2addnclem  37657  dvasin  37690  sdclem2  37728  totbndbnd  37775  ismgmOLD  37836  exidresid  37865  isrngo  37883  rngoablo2  37895  rngoueqz  37926  isdivrngo  37936  isdrngo1  37942  isdrngo2  37944  ispridl2  38024  relcnveq3  38302  elrelscnveq3  38472  ax12eq  38922  ax12el  38923  lkr0f  39075  hl2at  39387  dalemswapyz  39638  pclfinclN  39932  osumcllem11N  39948  pexmidlem8N  39959  ltrnnid  40118  aks4d1p8  42068  redvmptabs  42368  sn-00id  42407  rictr  42506  eu6w  42662  mptfcl  42707  fphpd  42803  elmnc  43124  itgoval  43149  arearect  43203  reabsifpos  43623  clsk3nimkb  44029  grumnud  44281  nanorxor  44300  pm11.71  44392  iotavalsb  44428  sbiota1  44429  2uasbanh  44558  eel0TT  44701  eelT00  44702  eelTTT  44703  eelT11  44704  eelT12  44706  eelTT1  44707  eelT01  44708  eel0T1  44709  eelTT  44768  uunT1p1  44778  uun121  44780  uun121p1  44781  un2122  44787  uunTT1  44790  uunTT1p1  44791  uunTT1p2  44792  uunT11  44793  uunT11p1  44794  uunT11p2  44795  uunT12  44796  uunT12p1  44797  uunT12p2  44798  uunT12p3  44799  uunT12p4  44800  uunT12p5  44801  uun111  44802  3anidm12p2  44804  uun123  44805  3impdirp1  44813  undif3VD  44879  ax6e2ndeqVD  44906  2uasbanhVD  44908  ax6e2ndeqALT  44928  iunconnlem2  44932  sineq0ALT  44934  modelaxreplem1  44942  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem3  45958  stoweidlem17  45972  fourierdlem42  46104  fourierdlem48  46109  fourierdlem50  46111  fourierdlem51  46112  fourierdlem76  46137  fourierdlem83  46144  fourierdlem87  46148  hoidmvval0  46542  rexrsb  47049  2reu8i  47062  2reuimp  47064  afv0nbfvbi  47100  afvfv0bi  47101  afveu  47102  fnbrafvb  47103  afvres  47121  tz6.12-afv  47122  dmfcoafv  47124  afvco2  47125  aovprc  47137  aovrcl  47138  aovmpt4g  47150  afv2eu  47187  afv2res  47188  tz6.12-afv2  47189  tz6.12i-afv2  47192  afv2rnfveq  47211  fvmptrab  47241  fvmptrabdm  47242  fzopred  47271  2ffzoeq  47276  elsprel  47399  prproropf1o  47431  reupr  47446  lighneal  47535  odd2prm2  47642  even3prm2  47643  grictr  47829  grlimgrtrilem2  47897  usgrexmpl12ngric  47932  upgrwlkupwlk  47983  ovn0ssdmfun  48002  islinindfis  48294  rrx2linest  48591  line2ylem  48600  mofeu  48677  isthincd2  48837  setrec2fun  48922  elsetrecslem  48929  setrecsres  48932  secval  48977  cscval  48978  cotval  48979