Theorem sylbir 227

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3imtr3i  283  ex  405  3expa  1098  3ori  1404  nanass  1486  19.38  1801  19.35  1840  sbi2  2236  sbi2vOLD  2247  nfeqf2  2306  nfeqf2OLD  2307  equsex  2353  sbi2ALT  2534  nexmoOLD  2549  dfmolem  2587  2mo  2679  axie2  2743  necon1bi  2995  necon1i  3000  r19.35  3282  sbhypf  3473  vtocl2OLD  3481  spc2ed  3520  reu6  3631  rabssrabd  3950  uneqin  4144  difin0ss  4216  inelcm  4298  falseral0  4343  raaan2  4348  difprsn1  4608  tppreqb  4613  n0snor2el  4639  unissint  4774  intminss  4776  iununi  4888  triin  5046  bm1.3ii  5064  eusv2nf  5150  reusv3i  5159  moabex  5209  copsex2g  5241  opelopabt  5274  eqrelrel  5521  opeliunxp2  5560  opelrn  5657  ssxpb  5873  xpima  5881  xpimasn  5884  dmsn0el  5909  relcoi2  5968  elsnxp  5982  reuop  5984  iotanul  6169  dffv2  6586  fnfvrnss  6709  fressnfv  6747  fconst5  6797  f1mpt  6846  isocnv3  6910  f1owe  6931  ovprc  7015  onminesb  7331  onminsb  7332  onintrab  7334  onnminsb  7337  onsucuni2  7367  tfindsg2  7394  zfrep6  7470  fo1stres  7529  fo2ndres  7530  bropopvvv  7595  bropfvvvv  7597  frxp  7627  opeliunxp2f  7681  mpoxopoveqd  7692  reldmtpos  7705  wfrlem4  7763  wfrlem4OLD  7764  wfrlem12  7772  wfrlem16  7776  wfr2  7780  tfrlem5  7822  tfrlem9  7827  tfr2  7840  rdgsuc  7866  oaordi  7975  oeordi  8016  omopthi  8086  fvmptmap  8246  mptelixpg  8298  ener  8355  domtr  8361  snfi  8393  unen  8395  xpf1o  8477  mapen  8479  unxpdomlem3  8521  isinf  8528  frfi  8560  unblem1  8567  unfi  8582  fofinf1o  8596  fsuppun  8649  inf3lem2  8888  inf3lem5  8891  cantnfp1lem1  8937  cantnfp1lem3  8939  tcmin  8979  r1ordg  9003  r1ord  9005  rankr1ai  9023  r1val3  9063  bndrank  9066  unbndrank  9067  rankr1b  9089  rankxplim3  9106  tcrank  9109  xpnum  9176  cardmin2  9223  infxpenlem  9235  fseqen  9249  dfac8clem  9254  alephsson  9322  alephfp  9330  dfac4  9344  kmlem6  9377  kmlem8  9379  kmlem9  9380  infpssr  9530  fin1a2lem12  9633  axcc4  9661  axcc4dom  9663  ac6s2  9708  zornn0g  9727  cardidg  9770  unsnen  9775  pwcfsdom  9805  cfpwsdom  9806  gchpwdom  9892  r1tskina  10004  intgru  10036  indpi  10129  nqereu  10151  supsrlem  10333  letrii  10567  dfnn3  11457  zaddcl  11838  nn0ind  11893  fnn0ind  11897  ublbneg  12150  nn01to3  12158  infmrp1  12556  fz0  12741  fzo1fzo0n0  12906  elfzom1elp1fzo  12922  fzo0end  12947  elfznelfzo  12960  fzind2  12973  injresinjlem  12975  fleqceilz  13040  nnsinds  13174  nn0sinds  13175  faclbnd4lem1  13471  hashinf  13513  hasheqf1oi  13530  hashgt0elex  13578  hashgt23el  13601  hashfacen  13628  hash2prde  13642  hash2sspr  13660  fun2dmnop0  13666  iswrddm0  13702  swrdn0OLD  13823  swrdnnn0nd  13827  swrdnd0  13828  swrdlsw  13848  pfxn0  13871  pfxnd0  13873  swrdswrdlem  13889  swrdccatin12lem3  13936  pfxccat3  13939  swrdccat3OLD  13940  pfxccat3a  13945  swrdccat3blem  13947  cshwsublen  14023  cshwidxmod  14030  repswcshw  14039  cshw1  14049  trclun  14238  dmtrclfv  14242  rediv  14354  imdiv  14361  sqrt0  14465  fsump1i  14987  modfsummods  15011  bpolydiflem  15271  bpoly3  15275  bpoly4  15276  cos1bnd  15403  sinltx  15405  rpnnen2lem1  15430  rpnnen2lem2  15431  rpnnen2lem12  15441  odd2np1  15553  opoe  15575  omoe  15576  opeo  15577  omeo  15578  gcdcllem1  15711  gcdaddmlem  15735  dfgcd2  15753  algfx  15783  lcmledvds  15802  lcmfunsnlem  15844  lcmfun  15848  coprmprod  15864  coprmproddvdslem  15865  odzval  15987  odzdvds  15991  prmreclem5  16115  mul4sq  16149  prmgaplem5  16250  prmgaplem6  16251  imasaddfnlem  16660  mreexexlem4d  16779  joindmss  17478  meetdmss  17492  gictr  18189  cntzval  18225  symg2bas  18290  odfval  18425  efgsfo  18627  efgrelexlemb  18639  dprddomcld  18876  dprdsubg  18899  dprd2da  18917  lssacs  19464  cnfldinv  20281  ocvval  20516  dmatmul  20813  mdetfval1  20906  mndifsplit  20952  fvmptnn04if  21164  toprntopon  21240  opnnei  21435  ordtbas2  21506  ordtrest2lem  21518  lmmo  21695  fincmp  21708  bwth  21725  txbas  21882  ptcnplem  21936  tx2ndc  21966  hmphtr  22098  fbun  22155  filconn  22198  ptcmplem5  22371  cnextcn  22382  utoptop  22549  ucncn  22600  metust  22874  cfilucfil  22875  elcncf1di  23209  xrhmeo  23256  phtpycc  23301  copco  23328  pcohtpylem  23329  pcopt  23332  pcopt2  23333  ncvsi  23461  ovolval  23780  iunmbl2  23864  itg2splitlem  24055  cpnfval  24235  plyval  24489  fta1  24603  aaliou2b  24636  tayl0  24656  ulmdvlem3  24696  radcnvlem2  24708  dvradcnv  24715  reeff1o  24741  sincosq1lem  24789  sincosq2sgn  24791  sincosq4sgn  24793  sinq12ge0  24800  logrncl  24855  eflog  24864  cxpge0  24970  logb1  25051  atanf  25162  atanbnd  25208  igamf  25333  igamcl  25334  lgsne0  25616  mul2sq  25700  2sqreultblem  25729  pntibnd  25874  ostth  25920  mptelee  26387  axlowdimlem9  26442  axlowdimlem12  26445  axcontlem2  26457  axcontlem12  26467  structgrssvtx  26515  structgrssiedg  26516  lpvtx  26559  nbuhgr  26831  nbumgr  26835  nbuhgr2vtx1edgblem  26839  nbgr0vtxlem  26843  nbgr1vtx  26846  uvtx01vtx  26885  prcliscplgr  26902  cusgrsizeinds  26940  sizusglecusglem2  26950  uhgrvd00  27022  fusgrregdegfi  27057  rusgr1vtxlem  27075  wlkeq  27121  wlk1walk  27126  uspgr2wlkeq  27133  wlklenvclwlk  27142  wlkreslem  27158  wlkreslemOLD  27160  wlkdlem2  27174  wlkdlem4  27176  spthonepeq  27244  clwlkclwwlkflem  27515  clwlkclwwlkfolem  27520  clwlkclwwlkfOLD  27521  clwlkclwwlkf  27525  clwwisshclwws  27533  clwwlkneq0  27547  3wlkdlem6  27697  eupth2eucrct  27750  eupth2lem1  27751  eupth2lem3lem7  27767  frgr3vlem1  27810  frgr3vlem2  27811  frgrncvvdeqlem8  27843  frgrncvvdeqlem9  27844  numclwwlk5  27948  frgrreg  27954  frgrregord013  27955  friendshipgt3  27958  isgrpo  28054  vciOLD  28118  vcex  28135  nmogtmnf  28327  siilem1  28408  siii  28410  ajmoi  28416  bcsiALT  28738  hhcms  28762  ocval  28841  hsupval  28895  omlsilem  28963  h1de2bi  29115  h1de2ctlem  29116  hosubeq0i  29387  adjmo  29393  nmopgtmnf  29429  nlfnval  29442  nmcopex  29590  nmcfnex  29614  riesz4i  29624  riesz1  29626  riesz2  29627  opsqrlem1  29701  superpos  29915  hatomistici  29923  chpssati  29924  mdsymlem3  29966  3o1cs  30011  3o2cs  30012  3o3cs  30013  iunrnmptss  30089  brabgaf  30126  f1mptrn  30145  ffsrn  30220  fpwrelmap  30224  xnn0gt0  30249  hashxpe  30279  fedgmul  30656  ordtrest2NEWlem  30809  qqhval2  30867  esumfsup  30973  esumcvg  30989  cntnevol  31132  ddemeas  31140  dya2icoseg2  31181  dya2iocnei  31185  eulerpartlems  31263  eulerpartlemgvv  31279  eulerpart  31285  cndprobprob  31342  ballotlemsdom  31415  ballotth  31441  sgn3da  31445  bnj945  31693  bnj1379  31750  bnj1459  31762  bnj557  31820  bnj571  31825  bnj849  31844  bnj964  31862  bnj978  31868  bnj1018  31881  bnj1020  31882  bnj1033  31886  bnj1175  31921  bnj1398  31951  bnj1417  31958  bnj1523  31988  txpconn  32064  msubco  32298  mclsax  32336  setinds  32543  dfon2lem7  32554  dfon2lem8  32555  poseq  32616  soseq  32617  frrlem4  32647  frr2  32666  nocvxminlem  32768  nocvxmin  32769  pprodss4v  32866  fullfunfv  32929  altxpsspw  32959  funtransport  33013  fvtransport  33014  funray  33122  fvray  33123  funline  33124  fvline  33126  finminlem  33187  bisym1  33287  onsucconni  33305  onsucsuccmpi  33311  bj-currypara  33412  bj-alcomexcom  33524  axc11n11r  33527  bj-equsal2  33639  bj-xpima1snALT  33765  bj-bm1.3ii  33866  mptsnunlem  34061  iooelexlt  34085  relowlpssretop  34087  rdgeqoa  34093  difunieq  34097  nlpineqsn  34130  fvineqsneq  34134  wl-lem-nexmo  34244  matunitlindflem1  34329  ptrecube  34333  poimirlem26  34359  poimirlem30  34363  poimir  34366  ismblfin  34374  itg2addnclem  34384  dvasin  34419  sdclem2  34459  totbndbnd  34509  ismgmOLD  34570  exidresid  34599  isrngo  34617  rngoablo2  34629  rngoueqz  34660  isdivrngo  34670  isdrngo1  34676  isdrngo2  34678  ispridl2  34758  relcnveq3  35022  elrelscnveq3  35176  ax12eq  35522  ax12el  35523  lkr0f  35675  hl2at  35986  dalemswapyz  36237  pclfinclN  36531  osumcllem11N  36547  pexmidlem8N  36558  ltrnnid  36717  mptfcl  38712  fphpd  38809  elmnc  39132  itgoval  39157  arearect  39218  clsk3nimkb  39753  grumnud  39997  nanorxor  40053  pm11.71  40146  iotavalsb  40182  sbiota1  40183  2uasbanh  40314  eel0TT  40457  eelT00  40458  eelTTT  40459  eelT11  40460  eelT12  40462  eelTT1  40463  eelT01  40464  eel0T1  40465  eelTT  40524  uunT1p1  40534  uun121  40536  uun121p1  40537  un2122  40543  uunTT1  40546  uunTT1p1  40547  uunTT1p2  40548  uunT11  40549  uunT11p1  40550  uunT11p2  40551  uunT12  40552  uunT12p1  40553  uunT12p2  40554  uunT12p3  40555  uunT12p4  40556  uunT12p5  40557  uun111  40558  3anidm12p2  40560  uun123  40561  3impdirp1  40569  undif3VD  40635  ax6e2ndeqVD  40662  2uasbanhVD  40664  ax6e2ndeqALT  40684  iunconnlem2  40688  sineq0ALT  40690  ioodvbdlimc1lem2  41648  ioodvbdlimc2lem  41650  stoweidlem3  41720  stoweidlem17  41734  fourierdlem42  41866  fourierdlem48  41871  fourierdlem50  41873  fourierdlem51  41874  fourierdlem76  41899  fourierdlem83  41906  fourierdlem87  41910  hoidmvval0  42301  rexrsb  42705  2reu8i  42719  2reuimp  42721  afv0nbfvbi  42757  afvfv0bi  42758  afveu  42759  fnbrafvb  42760  afvres  42778  tz6.12-afv  42779  dmfcoafv  42781  afvco2  42782  aovprc  42794  aovrcl  42795  aovmpt4g  42807  afv2eu  42844  afv2res  42845  tz6.12-afv2  42846  tz6.12i-afv2  42849  afv2rnfveq  42868  fvmptrab  42898  fvmptrabdm  42899  fzopred  42929  2ffzoeq  42935  ichan  42999  elsprel  43006  prproropf1o  43038  reupr  43053  lighneal  43145  odd2prm2  43252  even3prm2  43253  upgrwlkupwlk  43384  ovn0ssdmfun  43403  islinindfis  43872  rrx2linest  44098  line2ylem  44107  setrec2fun  44163  elsetrecslem  44169  setrecsres  44172  secval  44214  cscval  44215  cotval  44216