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 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3i  294  ex  416  3expa  1120  3ori  1426  nanass  1506  19.38  1846  19.35  1885  sbi2  2303  nfeqf2  2376  equsex  2417  dfmoeu  2535  2mo  2649  axie2  2703  necon1bi  2969  necon1i  2974  r19.35  3255  sbhypf  3467  spc2ed  3516  reu6  3639  rabssrabd  3996  uneqin  4193  difin0ss  4283  inelcm  4379  rzal  4420  ralf0  4425  falseral0  4431  raaan2  4436  difprsn1  4713  tppreqb  4718  n0snor2el  4744  unissint  4883  intminss  4885  iununi  5007  triin  5176  bm1.3ii  5195  eusv2nf  5288  reusv3i  5297  moabex  5343  copsex2gOLD  5377  opelopabt  5413  eqrelrel  5667  opeliunxp2  5707  opelrn  5812  ssxpb  6037  xpima  6045  xpimasn  6048  dmsn0el  6074  relcnvtr  6131  relcoi2  6140  elsnxp  6154  reuop  6156  iotanul  6358  dffv2  6806  fnfvrnss  6937  fressnfv  6975  fconst5  7021  f1mpt  7073  isocnv3  7141  f1owe  7162  ovprc  7251  fvmpopr2d  7370  onminesb  7577  onminsb  7578  onintrab  7580  onnminsb  7583  onsucuni2  7613  tfindsg2  7640  zfrep6  7728  fo1stres  7787  fo2ndres  7788  bropopvvv  7858  bropfvvvv  7860  frxp  7893  opeliunxp2f  7952  mpoxopoveqd  7963  reldmtpos  7976  frrlem4  8030  wfrlem4  8058  wfrlem12  8066  wfrlem16  8070  wfr2  8074  tfrlem5  8116  tfrlem9  8121  tfr2  8134  rdgsuc  8160  oaordi  8274  oeordi  8315  omopthi  8386  fvmptmap  8562  mptelixpg  8616  ener  8675  domtr  8681  snfi  8721  unen  8723  xpf1o  8808  mapen  8810  rexdif1en  8839  dif1en  8840  pssnn  8846  unfi  8850  ssfi  8851  ensymfib  8862  entrfil  8863  enfii  8864  unxpdomlem3  8884  isinf  8891  frfi  8916  unblem1  8923  unfiOLD  8938  fofinf1o  8951  fsuppun  9004  inf3lem2  9244  inf3lem5  9247  cantnfp1lem1  9293  cantnfp1lem3  9295  tcmin  9357  frr2  9376  r1ordg  9394  r1ord  9396  rankr1ai  9414  r1val3  9454  bndrank  9457  unbndrank  9458  rankr1b  9480  rankxplim3  9497  tcrank  9500  xpnum  9567  cardmin2  9615  infxpenlem  9627  fseqen  9641  dfac8clem  9646  alephsson  9714  alephfp  9722  dfac4  9736  kmlem6  9769  kmlem8  9771  kmlem9  9772  infpssr  9922  fin1a2lem12  10025  axcc4  10053  axcc4dom  10055  ac6s2  10100  zornn0g  10119  cardidg  10162  unsnen  10167  pwcfsdom  10197  cfpwsdom  10198  gchpwdom  10284  r1tskina  10396  intgru  10428  indpi  10521  nqereu  10543  supsrlem  10725  letrii  10957  dfnn3  11844  zaddcl  12217  nn0ind  12272  fnn0ind  12276  ublbneg  12529  nn01to3  12537  infmrp1  12934  fz0  13127  fzo1fzo0n0  13293  elfzom1elp1fzo  13309  fzo0end  13334  elfznelfzo  13347  fzind2  13360  injresinjlem  13362  fleqceilz  13427  nnsinds  13561  nn0sinds  13562  faclbnd4lem1  13859  hashinf  13901  hasheqf1oi  13918  hashgt0elex  13968  hashgt23el  13991  hashfacen  14018  hashfacenOLD  14019  hash2prde  14036  hash2sspr  14054  fun2dmnop0  14060  iswrddm0  14093  swrdnnn0nd  14221  swrdnd0  14222  swrdlsw  14232  pfxn0  14251  pfxnd0  14253  swrdswrdlem  14269  pfxccatin12lem3  14297  pfxccat3  14299  pfxccat3a  14303  swrdccat3blem  14304  cshwsublen  14361  cshwidxmod  14368  repswcshw  14377  cshw1  14387  trclun  14577  dmtrclfv  14581  rediv  14694  imdiv  14701  sqrt0  14805  fsump1i  15333  modfsummods  15357  bpolydiflem  15616  bpoly3  15620  bpoly4  15621  cos1bnd  15748  sinltx  15750  rpnnen2lem1  15775  rpnnen2lem2  15776  rpnnen2lem12  15786  odd2np1  15902  opoe  15924  omoe  15925  opeo  15926  omeo  15927  gcdcllem1  16058  gcdaddmlem  16083  dfgcd2  16106  algfx  16137  lcmledvds  16156  lcmfunsnlem  16198  lcmfun  16202  coprmprod  16218  coprmproddvdslem  16219  odzval  16344  odzdvds  16348  prmreclem5  16473  mul4sq  16507  prmgaplem5  16608  prmgaplem6  16609  imasaddfnlem  17033  mreexexlem4d  17150  joindmss  17885  meetdmss  17899  gictr  18679  cntzval  18715  symg2bas  18785  odfval  18924  efgsfo  19129  efgrelexlemb  19140  dprddomcld  19388  dprdsubg  19411  dprd2da  19429  lssacs  20004  cnfldinv  20394  ocvval  20629  selvval  21078  dmatmul  21394  mdetfval1  21487  mndifsplit  21533  fvmptnn04if  21746  toprntopon  21822  opnnei  22017  ordtbas2  22088  ordtrest2lem  22100  lmmo  22277  fincmp  22290  bwth  22307  txbas  22464  ptcnplem  22518  tx2ndc  22548  hmphtr  22680  fbun  22737  filconn  22780  ptcmplem5  22953  cnextcn  22964  utoptop  23132  ucncn  23182  metust  23456  cfilucfil  23457  elcncf1di  23792  xrhmeo  23843  phtpycc  23888  copco  23915  pcohtpylem  23916  pcopt  23919  pcopt2  23920  ncvsi  24048  ovolval  24370  iunmbl2  24454  itg2splitlem  24646  cpnfval  24829  plyval  25087  fta1  25201  aaliou2b  25234  tayl0  25254  ulmdvlem3  25294  radcnvlem2  25306  dvradcnv  25313  reeff1o  25339  sincosq1lem  25387  sincosq2sgn  25389  sincosq4sgn  25391  sinq12ge0  25398  logrncl  25456  eflog  25465  cxpge0  25571  logb1  25652  atanf  25763  atanbnd  25809  igamf  25933  igamcl  25934  lgsne0  26216  mul2sq  26300  2sqreultblem  26329  pntibnd  26474  ostth  26520  mptelee  26986  axlowdimlem9  27041  axlowdimlem12  27044  axcontlem2  27056  axcontlem12  27066  structgrssvtx  27115  structgrssiedg  27116  lpvtx  27159  nbuhgr  27431  nbumgr  27435  nbuhgr2vtx1edgblem  27439  nbgr0vtxlem  27443  nbgr1vtx  27446  uvtx01vtx  27485  prcliscplgr  27502  cusgrsizeinds  27540  sizusglecusglem2  27550  uhgrvd00  27622  fusgrregdegfi  27657  rusgr1vtxlem  27675  wlkeq  27721  wlk1walk  27726  uspgr2wlkeq  27733  wlklenvclwlk  27742  wlklenvclwlkOLD  27743  wlkreslem  27757  wlkdlem2  27771  wlkdlem4  27773  spthonepeq  27839  clwlkclwwlkflem  28087  clwlkclwwlkfolem  28090  clwlkclwwlkf  28091  clwwisshclwws  28098  clwwlkneq0  28112  3wlkdlem6  28248  eupth2eucrct  28300  eupth2lem1  28301  eupth2lem3lem7  28317  frgr3vlem1  28356  frgr3vlem2  28357  frgrncvvdeqlem8  28389  frgrncvvdeqlem9  28390  numclwwlk5  28471  frgrreg  28477  frgrregord013  28478  friendshipgt3  28481  isgrpo  28578  vciOLD  28642  vcex  28659  nmogtmnf  28851  siilem1  28932  siii  28934  ajmoi  28939  bcsiALT  29260  hhcms  29284  ocval  29361  hsupval  29415  omlsilem  29483  h1de2bi  29635  h1de2ctlem  29636  hosubeq0i  29907  adjmo  29913  nmopgtmnf  29949  nlfnval  29962  nmcopex  30110  nmcfnex  30134  riesz4i  30144  riesz1  30146  riesz2  30147  opsqrlem1  30221  superpos  30435  hatomistici  30443  chpssati  30444  mdsymlem3  30486  3o1cs  30531  3o2cs  30532  3o3cs  30533  iunrnmptss  30624  brabgaf  30667  f1mptrn  30689  ffsrn  30784  fpwrelmap  30788  xnn0gt0  30812  hashxpe  30847  prmidl2  31330  mxidlnzrb  31358  fedgmul  31426  ordtrest2NEWlem  31586  qqhval2  31644  esumfsup  31750  esumcvg  31766  cntnevol  31908  ddemeas  31916  dya2icoseg2  31957  dya2iocnei  31961  eulerpartlems  32039  eulerpartlemgvv  32055  eulerpart  32061  cndprobprob  32117  ballotlemsdom  32190  ballotth  32216  sgn3da  32220  bnj945  32466  bnj1379  32523  bnj1459  32536  bnj557  32594  bnj571  32599  bnj849  32618  bnj964  32636  bnj978  32642  bnj1018g  32656  bnj1018  32657  bnj1020  32658  bnj1033  32662  bnj1175  32697  bnj1398  32727  bnj1417  32734  bnj1523  32764  nummin  32776  cusgr3cyclex  32811  txpconn  32907  satfv1  33038  satffun  33084  msubco  33206  mclsax  33244  setinds  33473  dfon2lem7  33484  dfon2lem8  33485  poseq  33539  soseq  33540  on2recsov  33564  nocvxminlem  33709  nocvxmin  33710  norec2ov  33851  pprodss4v  33923  fullfunfv  33986  altxpsspw  34016  funtransport  34070  fvtransport  34071  funray  34179  fvray  34180  funline  34181  fvline  34183  finminlem  34244  bisym1  34345  onsucconni  34363  onsucsuccmpi  34369  bj-currypara  34477  bj-alcomexcom  34599  axc11n11r  34602  bj-equsal2  34745  bj-xpima1snALT  34884  bj-bm1.3ii  34972  bj-opelidb1ALT  35072  mptsnunlem  35246  iooelexlt  35270  relowlpssretop  35272  rdgeqoa  35278  difunieq  35282  nlpineqsn  35316  fvineqsneq  35320  wl-lem-nexmo  35459  matunitlindflem1  35510  ptrecube  35514  poimirlem26  35540  poimirlem30  35544  poimir  35547  ismblfin  35555  itg2addnclem  35565  dvasin  35598  sdclem2  35637  totbndbnd  35684  ismgmOLD  35745  exidresid  35774  isrngo  35792  rngoablo2  35804  rngoueqz  35835  isdivrngo  35845  isdrngo1  35851  isdrngo2  35853  ispridl2  35933  relcnveq3  36193  elrelscnveq3  36346  ax12eq  36692  ax12el  36693  lkr0f  36845  hl2at  37156  dalemswapyz  37407  pclfinclN  37701  osumcllem11N  37717  pexmidlem8N  37728  ltrnnid  37887  19.8aw  39900  sn-00id  40092  mptfcl  40245  fphpd  40341  elmnc  40664  itgoval  40689  arearect  40749  reabsifpos  40918  clsk3nimkb  41327  grumnud  41577  nanorxor  41596  pm11.71  41688  iotavalsb  41724  sbiota1  41725  2uasbanh  41854  eel0TT  41997  eelT00  41998  eelTTT  41999  eelT11  42000  eelT12  42002  eelTT1  42003  eelT01  42004  eel0T1  42005  eelTT  42064  uunT1p1  42074  uun121  42076  uun121p1  42077  un2122  42083  uunTT1  42086  uunTT1p1  42087  uunTT1p2  42088  uunT11  42089  uunT11p1  42090  uunT11p2  42091  uunT12  42092  uunT12p1  42093  uunT12p2  42094  uunT12p3  42095  uunT12p4  42096  uunT12p5  42097  uun111  42098  3anidm12p2  42100  uun123  42101  3impdirp1  42109  undif3VD  42175  ax6e2ndeqVD  42202  2uasbanhVD  42204  ax6e2ndeqALT  42224  iunconnlem2  42228  sineq0ALT  42230  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  stoweidlem3  43219  stoweidlem17  43233  fourierdlem42  43365  fourierdlem48  43370  fourierdlem50  43372  fourierdlem51  43373  fourierdlem76  43398  fourierdlem83  43405  fourierdlem87  43409  hoidmvval0  43800  rexrsb  44264  2reu8i  44277  2reuimp  44279  afv0nbfvbi  44315  afvfv0bi  44316  afveu  44317  fnbrafvb  44318  afvres  44336  tz6.12-afv  44337  dmfcoafv  44339  afvco2  44340  aovprc  44352  aovrcl  44353  aovmpt4g  44365  afv2eu  44402  afv2res  44403  tz6.12-afv2  44404  tz6.12i-afv2  44407  afv2rnfveq  44426  fvmptrab  44456  fvmptrabdm  44457  fzopred  44487  2ffzoeq  44493  elsprel  44600  prproropf1o  44632  reupr  44647  lighneal  44736  odd2prm2  44843  even3prm2  44844  upgrwlkupwlk  44975  ovn0ssdmfun  44994  islinindfis  45463  rrx2linest  45761  line2ylem  45770  mofeu  45848  isthincd2  45992  setrec2fun  46069  elsetrecslem  46075  setrecsres  46078  secval  46120  cscval  46121  cotval  46122