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  290  ex  413  3expa  1118  3ori  1424  nanass  1508  19.38  1841  19.35  1880  19.8aw  2053  equsexv  2259  sbi2  2298  nfeqf2  2376  equsex  2417  dfmoeu  2530  2mo  2644  axie2  2698  necon1bi  2969  necon1i  2974  r19.35  3108  r19.35OLD  3109  sbhypfOLD  3539  spc2ed  3591  reu6  3721  rabssrabd  4080  uneqin  4277  difin0ss  4367  inelcm  4463  rzal  4507  ralf0  4512  falseral0  4518  raaan2  4523  difprsn1  4802  tppreqb  4807  n0snor2el  4833  unissint  4975  intminss  4977  dfiun2g  5032  iununi  5101  triin  5281  bm1.3ii  5301  eusv2nf  5392  reusv3i  5401  moabex  5458  copsex2gOLD  5493  opelopabt  5531  eqrelrel  5795  opeliunxp2  5836  opelrn  5940  ssxpb  6170  xpima  6178  xpimasn  6181  dmsn0el  6207  relcnvtr  6263  relcoi2  6273  elsnxp  6287  reuop  6289  iotanul  6518  dffv2  6983  fnfvrnss  7116  fressnfv  7154  fconst5  7203  f1mpt  7256  isocnv3  7325  f1owe  7346  ovprc  7443  fvmpopr2d  7565  onminesb  7777  onminsb  7778  onintrab  7780  onnminsb  7783  ordsuci  7792  onsucuni2  7818  tfindsg2  7847  zfrep6  7937  fo1stres  7997  fo2ndres  7998  bropopvvv  8072  bropfvvvv  8074  frxp  8108  poseq  8140  soseq  8141  opeliunxp2f  8191  mpoxopoveqd  8202  reldmtpos  8215  frrlem4  8270  wfrlem4OLD  8308  wfrlem12OLD  8316  wfrlem16OLD  8320  wfr2OLD  8324  tfrlem5  8376  tfrlem9  8381  tfr2  8394  rdgsuc  8420  oaordi  8542  oeordi  8583  omopthi  8656  on2recsov  8663  fvmptmap  8871  mptelixpg  8925  ener  8993  domtr  8999  snfi  9040  unen  9042  undom  9055  dom0  9098  xpf1o  9135  mapen  9137  rexdif1enOLD  9155  dif1enOLD  9158  pssnn  9164  unfi  9168  ssfi  9169  ensymfib  9183  entrfil  9184  enfii  9185  domtrfil  9191  unxpdomlem3  9248  isinf  9256  isinfOLD  9257  frfi  9284  unblem1  9291  unfiOLD  9309  fofinf1o  9323  fsuppun  9378  inf3lem2  9620  inf3lem5  9623  cantnfp1lem1  9669  cantnfp1lem3  9671  tcmin  9732  frr2  9751  r1ordg  9769  r1ord  9771  rankr1ai  9789  r1val3  9829  bndrank  9832  unbndrank  9833  rankr1b  9855  rankxplim3  9872  tcrank  9875  xpnum  9942  cardmin2  9990  infxpenlem  10004  fseqen  10018  dfac8clem  10023  alephsson  10091  alephfp  10099  dfac4  10113  kmlem6  10146  kmlem8  10148  kmlem9  10149  infpssr  10299  fin1a2lem12  10402  axcc4  10430  axcc4dom  10432  ac6s2  10477  zornn0g  10496  cardidg  10539  unsnen  10544  pwcfsdom  10574  cfpwsdom  10575  gchpwdom  10661  r1tskina  10773  intgru  10805  indpi  10898  nqereu  10920  supsrlem  11102  letrii  11335  dfnn3  12222  zaddcl  12598  nn0ind  12653  fnn0ind  12657  ublbneg  12913  nn01to3  12921  infmrp1  13319  fz0  13512  fzo1fzo0n0  13679  elfzom1elp1fzo  13695  fzo0end  13720  elfznelfzo  13733  fzind2  13746  injresinjlem  13748  fleqceilz  13815  nnsinds  13949  nn0sinds  13950  faclbnd4lem1  14249  hashinf  14291  hasheqf1oi  14307  hashgt0elex  14357  hashgt23el  14380  hashfacen  14409  hashfacenOLD  14410  hash2prde  14427  hash2sspr  14445  fun2dmnop0  14451  iswrddm0  14484  swrdnnn0nd  14602  swrdnd0  14603  swrdlsw  14613  pfxn0  14632  pfxnd0  14634  swrdswrdlem  14650  pfxccatin12lem3  14678  pfxccat3  14680  pfxccat3a  14684  swrdccat3blem  14685  cshwsublen  14742  cshwidxmod  14749  repswcshw  14758  cshw1  14768  trclun  14957  dmtrclfv  14961  rediv  15074  imdiv  15081  fsump1i  15711  modfsummods  15735  bpolydiflem  15994  bpoly3  15998  bpoly4  15999  cos1bnd  16126  sinltx  16128  rpnnen2lem1  16153  rpnnen2lem2  16154  rpnnen2lem12  16164  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  gcdcllem1  16436  gcdaddmlem  16461  dfgcd2  16484  algfx  16513  lcmledvds  16532  lcmfunsnlem  16574  lcmfun  16578  coprmprod  16594  coprmproddvdslem  16595  odzval  16720  odzdvds  16724  prmreclem5  16849  mul4sq  16883  prmgaplem5  16984  prmgaplem6  16985  imasaddfnlem  17470  mreexexlem4d  17587  joindmss  18328  meetdmss  18342  gictr  19143  cntzval  19179  symg2bas  19254  odfval  19394  efgsfo  19601  efgrelexlemb  19612  dprddomcld  19865  dprdsubg  19888  dprd2da  19906  lssacs  20570  cnfldinv  20968  ocvval  21211  selvval  21672  dmatmul  21990  mdetfval1  22083  mndifsplit  22129  fvmptnn04if  22342  toprntopon  22418  opnnei  22615  ordtbas2  22686  ordtrest2lem  22698  lmmo  22875  fincmp  22888  bwth  22905  txbas  23062  ptcnplem  23116  tx2ndc  23146  hmphtr  23278  fbun  23335  filconn  23378  ptcmplem5  23551  cnextcn  23562  utoptop  23730  ucncn  23781  metust  24058  cfilucfil  24059  elcncf1di  24402  xrhmeo  24453  phtpycc  24498  copco  24525  pcohtpylem  24526  pcopt  24529  pcopt2  24530  ncvsi  24659  ovolval  24981  iunmbl2  25065  itg2splitlem  25257  cpnfval  25440  plyval  25698  fta1  25812  aaliou2b  25845  tayl0  25865  ulmdvlem3  25905  radcnvlem2  25917  dvradcnv  25924  reeff1o  25950  sincosq1lem  25998  sincosq2sgn  26000  sincosq4sgn  26002  sinq12ge0  26009  logrncl  26067  eflog  26076  cxpge0  26182  logb1  26263  atanf  26374  atanbnd  26420  igamf  26544  igamcl  26545  lgsne0  26827  mul2sq  26911  2sqreultblem  26940  pntibnd  27085  ostth  27131  nocvxminlem  27268  nocvxmin  27269  cutlt  27408  norec2ov  27430  addsuniflem  27473  mulsuniflem  27593  mptelee  28142  axlowdimlem9  28197  axlowdimlem12  28200  axcontlem2  28212  axcontlem12  28222  structgrssvtx  28273  structgrssiedg  28274  lpvtx  28317  nbuhgr  28589  nbumgr  28593  nbuhgr2vtx1edgblem  28597  nbgr0vtxlem  28601  nbgr1vtx  28604  uvtx01vtx  28643  prcliscplgr  28660  cusgrsizeinds  28698  sizusglecusglem2  28708  uhgrvd00  28780  fusgrregdegfi  28815  rusgr1vtxlem  28833  wlkeq  28880  wlk1walk  28885  uspgr2wlkeq  28892  wlklenvclwlk  28901  wlkreslem  28915  wlkdlem2  28929  wlkdlem4  28931  spthonepeq  28998  clwlkclwwlkflem  29246  clwlkclwwlkfolem  29249  clwlkclwwlkf  29250  clwwisshclwws  29257  clwwlkneq0  29271  3wlkdlem6  29407  eupth2eucrct  29459  eupth2lem1  29460  eupth2lem3lem7  29476  frgr3vlem1  29515  frgr3vlem2  29516  frgrncvvdeqlem8  29548  frgrncvvdeqlem9  29549  numclwwlk5  29630  frgrreg  29636  frgrregord013  29637  friendshipgt3  29640  isgrpo  29737  vciOLD  29801  vcex  29818  nmogtmnf  30010  siilem1  30091  siii  30093  ajmoi  30098  bcsiALT  30419  hhcms  30443  ocval  30520  hsupval  30574  omlsilem  30642  h1de2bi  30794  h1de2ctlem  30795  hosubeq0i  31066  adjmo  31072  nmopgtmnf  31108  nlfnval  31121  nmcopex  31269  nmcfnex  31293  riesz4i  31303  riesz1  31305  riesz2  31306  opsqrlem1  31380  superpos  31594  hatomistici  31602  chpssati  31603  mdsymlem3  31645  3o1cs  31690  3o2cs  31691  3o3cs  31692  iunrnmptss  31784  brabgaf  31824  f1mptrn  31846  ffsrn  31941  fpwrelmap  31945  xnn0gt0  31969  hashxpe  32006  prmidl2  32547  mxidlnzrb  32583  fedgmul  32704  ordtrest2NEWlem  32890  qqhval2  32950  esumfsup  33056  esumcvg  33072  cntnevol  33214  ddemeas  33222  dya2icoseg2  33265  dya2iocnei  33269  eulerpartlems  33347  eulerpartlemgvv  33363  eulerpart  33369  cndprobprob  33425  ballotlemsdom  33498  ballotth  33524  sgn3da  33528  bnj945  33772  bnj1379  33829  bnj1459  33842  bnj557  33900  bnj571  33905  bnj849  33924  bnj964  33942  bnj978  33948  bnj1018g  33962  bnj1018  33963  bnj1020  33964  bnj1033  33968  bnj1175  34003  bnj1398  34033  bnj1417  34040  bnj1523  34070  nummin  34082  cusgr3cyclex  34115  txpconn  34211  satfv1  34342  satffun  34388  msubco  34510  mclsax  34548  setinds  34738  dfon2lem7  34749  dfon2lem8  34750  pprodss4v  34844  fullfunfv  34907  altxpsspw  34937  funtransport  34991  fvtransport  34992  funray  35100  fvray  35101  funline  35102  fvline  35104  finminlem  35191  bisym1  35292  onsucconni  35310  onsucsuccmpi  35316  bj-currypara  35424  axc11n11r  35549  bj-equsal2  35691  bj-xpima1snALT  35826  bj-unexg  35907  bj-bm1.3ii  35933  bj-opelidb1ALT  36035  mptsnunlem  36207  iooelexlt  36231  relowlpssretop  36233  rdgeqoa  36239  difunieq  36243  nlpineqsn  36277  fvineqsneq  36281  wl-lem-nexmo  36420  matunitlindflem1  36472  ptrecube  36476  poimirlem26  36502  poimirlem30  36506  poimir  36509  ismblfin  36517  itg2addnclem  36527  dvasin  36560  sdclem2  36598  totbndbnd  36645  ismgmOLD  36706  exidresid  36735  isrngo  36753  rngoablo2  36765  rngoueqz  36796  isdivrngo  36806  isdrngo1  36812  isdrngo2  36814  ispridl2  36894  relcnveq3  37178  elrelscnveq3  37349  ax12eq  37799  ax12el  37800  lkr0f  37952  hl2at  38264  dalemswapyz  38515  pclfinclN  38809  osumcllem11N  38825  pexmidlem8N  38836  ltrnnid  38995  aks4d1p8  40940  rictr  41092  sn-00id  41270  mptfcl  41443  fphpd  41539  elmnc  41863  itgoval  41888  arearect  41949  reabsifpos  42370  clsk3nimkb  42776  grumnud  43030  nanorxor  43049  pm11.71  43141  iotavalsb  43177  sbiota1  43178  2uasbanh  43307  eel0TT  43450  eelT00  43451  eelTTT  43452  eelT11  43453  eelT12  43455  eelTT1  43456  eelT01  43457  eel0T1  43458  eelTT  43517  uunT1p1  43527  uun121  43529  uun121p1  43530  un2122  43536  uunTT1  43539  uunTT1p1  43540  uunTT1p2  43541  uunT11  43542  uunT11p1  43543  uunT11p2  43544  uunT12  43545  uunT12p1  43546  uunT12p2  43547  uunT12p3  43548  uunT12p4  43549  uunT12p5  43550  uun111  43551  3anidm12p2  43553  uun123  43554  3impdirp1  43562  undif3VD  43628  ax6e2ndeqVD  43655  2uasbanhVD  43657  ax6e2ndeqALT  43677  iunconnlem2  43681  sineq0ALT  43683  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  stoweidlem3  44705  stoweidlem17  44719  fourierdlem42  44851  fourierdlem48  44856  fourierdlem50  44858  fourierdlem51  44859  fourierdlem76  44884  fourierdlem83  44891  fourierdlem87  44895  hoidmvval0  45289  rexrsb  45794  2reu8i  45807  2reuimp  45809  afv0nbfvbi  45845  afvfv0bi  45846  afveu  45847  fnbrafvb  45848  afvres  45866  tz6.12-afv  45867  dmfcoafv  45869  afvco2  45870  aovprc  45882  aovrcl  45883  aovmpt4g  45895  afv2eu  45932  afv2res  45933  tz6.12-afv2  45934  tz6.12i-afv2  45937  afv2rnfveq  45956  fvmptrab  45986  fvmptrabdm  45987  fzopred  46016  2ffzoeq  46022  elsprel  46129  prproropf1o  46161  reupr  46176  lighneal  46265  odd2prm2  46372  even3prm2  46373  upgrwlkupwlk  46504  ovn0ssdmfun  46523  islinindfis  47083  rrx2linest  47381  line2ylem  47390  mofeu  47467  isthincd2  47611  setrec2fun  47690  elsetrecslem  47697  setrecsres  47700  secval  47745  cscval  47746  cotval  47747