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  1424  nanass  1507  19.38  1837  19.35  1876  19.8aw  2050  equsexv  2269  sbi2  2306  nfeqf2  2385  equsex  2426  dfmoeu  2539  2mo  2651  axie2  2706  necon1bi  2975  necon1i  2980  r19.35  3114  r19.35OLD  3115  sbhypfOLD  3557  spc2ed  3614  reu6  3748  rabssrabd  4106  uneqin  4308  difin0ss  4396  inelcm  4488  rzal  4532  ralf0  4537  falseral0  4539  raaan2  4544  difprsn1  4825  tppreqb  4830  n0snor2el  4858  unissint  4996  intminss  4998  dfiun2g  5053  iununi  5122  triin  5300  bm1.3ii  5320  eusv2nf  5413  reusv3i  5422  moabex  5479  opelopabt  5551  eqrelrel  5821  opeliunxp2  5863  opelrn  5968  ssxpb  6205  xpima  6213  xpimasn  6216  dmsn0el  6242  relcnvtr  6298  relcoi2  6308  elsnxp  6322  reuop  6324  iotanul  6551  dffv2  7017  fnfvrnss  7155  fressnfv  7194  fconst5  7243  f1mpt  7298  isocnv3  7368  f1owe  7389  ovprc  7486  fvmpopr2d  7612  onminesb  7829  onminsb  7830  onintrab  7832  onnminsb  7835  ordsuci  7844  onsucuni2  7870  tfindsg2  7899  zfrep6  7995  fo1stres  8056  fo2ndres  8057  bropopvvv  8131  bropfvvvv  8133  frxp  8167  poseq  8199  soseq  8200  opeliunxp2f  8251  mpoxopoveqd  8262  reldmtpos  8275  frrlem4  8330  wfrlem4OLD  8368  wfrlem12OLD  8376  wfrlem16OLD  8380  wfr2OLD  8384  tfrlem5  8436  tfrlem9  8441  tfr2  8454  rdgsuc  8480  oaordi  8602  oeordi  8643  omopthi  8717  on2recsov  8724  fvmptmap  8939  mptelixpg  8993  ener  9061  domtr  9067  snfiOLD  9110  unen  9112  undom  9125  dom0  9168  xpf1o  9205  mapen  9207  rexdif1enOLD  9225  dif1enOLD  9228  pssnn  9234  unfi  9238  ssfi  9240  ensymfib  9250  entrfil  9251  enfii  9252  domtrfil  9258  unxpdomlem3  9315  isinf  9323  isinfOLD  9324  frfi  9349  unblem1  9356  fofinf1o  9400  fsuppun  9456  inf3lem2  9698  inf3lem5  9701  cantnfp1lem1  9747  cantnfp1lem3  9749  tcmin  9810  frr2  9829  r1ordg  9847  r1ord  9849  rankr1ai  9867  r1val3  9907  bndrank  9910  unbndrank  9911  rankr1b  9933  rankxplim3  9950  tcrank  9953  xpnum  10020  cardmin2  10068  infxpenlem  10082  fseqen  10096  dfac8clem  10101  alephsson  10169  alephfp  10177  dfac4  10191  kmlem6  10225  kmlem8  10227  kmlem9  10228  cflem  10314  infpssr  10377  fin1a2lem12  10480  axcc4  10508  axcc4dom  10510  ac6s2  10555  zornn0g  10574  cardidg  10617  unsnen  10622  pwcfsdom  10652  cfpwsdom  10653  gchpwdom  10739  r1tskina  10851  intgru  10883  indpi  10976  nqereu  10998  supsrlem  11180  letrii  11415  dfnn3  12307  zaddcl  12683  nn0ind  12738  fnn0ind  12742  ublbneg  12998  nn01to3  13006  infmrp1  13406  fz0  13599  fzo1fzo0n0  13767  elfzom1elp1fzo  13783  fzo0end  13808  elfznelfzo  13822  fzind2  13835  injresinjlem  13837  fleqceilz  13905  nnsinds  14039  nn0sinds  14040  faclbnd4lem1  14342  hashinf  14384  hasheqf1oi  14400  hashgt0elex  14450  hashgt23el  14473  hashfacen  14503  hash2prde  14519  hash2sspr  14538  fun2dmnop0  14553  iswrddm0  14586  swrdnnn0nd  14704  swrdnd0  14705  swrdlsw  14715  pfxn0  14734  pfxnd0  14736  swrdswrdlem  14752  pfxccatin12lem3  14780  pfxccat3  14782  pfxccat3a  14786  swrdccat3blem  14787  cshwsublen  14844  cshwidxmod  14851  repswcshw  14860  cshw1  14870  trclun  15063  dmtrclfv  15067  rediv  15180  imdiv  15187  fsump1i  15817  modfsummods  15841  bpolydiflem  16102  bpoly3  16106  bpoly4  16107  cos1bnd  16235  sinltx  16237  rpnnen2lem1  16262  rpnnen2lem2  16263  rpnnen2lem12  16273  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  gcdcllem1  16545  gcdaddmlem  16570  dfgcd2  16593  algfx  16627  lcmledvds  16646  lcmfunsnlem  16688  lcmfun  16692  coprmprod  16708  coprmproddvdslem  16709  odzval  16838  odzdvds  16842  prmreclem5  16967  mul4sq  17001  prmgaplem5  17102  prmgaplem6  17103  imasaddfnlem  17588  mreexexlem4d  17705  joindmss  18449  meetdmss  18463  gictr  19316  cntzval  19361  symg2bas  19434  odfval  19574  efgsfo  19781  efgrelexlemb  19792  dprddomcld  20045  dprdsubg  20068  dprd2da  20086  lssacs  20988  cnfldinv  21438  pzriprnglem7  21521  ocvval  21708  selvval  22162  dmatmul  22524  mdetfval1  22617  mndifsplit  22663  fvmptnn04if  22876  toprntopon  22952  opnnei  23149  ordtbas2  23220  ordtrest2lem  23232  lmmo  23409  fincmp  23422  bwth  23439  txbas  23596  ptcnplem  23650  tx2ndc  23680  hmphtr  23812  fbun  23869  filconn  23912  ptcmplem5  24085  cnextcn  24096  utoptop  24264  ucncn  24315  metust  24592  cfilucfil  24593  elcncf1di  24940  xrhmeo  24996  phtpycc  25042  copco  25070  pcohtpylem  25071  pcopt  25074  pcopt2  25075  ncvsi  25204  ovolval  25527  iunmbl2  25611  itg2splitlem  25803  cpnfval  25988  plyval  26252  fta1  26368  aaliou2b  26401  tayl0  26421  ulmdvlem3  26463  radcnvlem2  26475  dvradcnv  26482  reeff1o  26509  sincosq1lem  26557  sincosq2sgn  26559  sincosq4sgn  26561  sinq12ge0  26568  logrncl  26627  eflog  26636  cxpge0  26743  logb1  26830  atanf  26941  atanbnd  26987  igamf  27112  igamcl  27113  lgsne0  27397  mul2sq  27481  2sqreultblem  27510  pntibnd  27655  ostth  27701  nocvxminlem  27840  nocvxmin  27841  cutlt  27984  norec2ov  28008  addsuniflem  28052  mulsuniflem  28193  zmulscld  28401  zseo  28424  mptelee  28928  axlowdimlem9  28983  axlowdimlem12  28986  axcontlem2  28998  axcontlem12  29008  structgrssvtx  29059  structgrssiedg  29060  lpvtx  29103  nbuhgr  29378  nbumgr  29382  nbuhgr2vtx1edgblem  29386  nbgr0edglem  29391  nbgr1vtx  29393  uvtx01vtx  29432  prcliscplgr  29449  cusgrsizeinds  29488  sizusglecusglem2  29498  uhgrvd00  29570  fusgrregdegfi  29605  rusgr1vtxlem  29623  wlkeq  29670  wlk1walk  29675  uspgr2wlkeq  29682  wlklenvclwlk  29691  wlkreslem  29705  wlkdlem2  29719  wlkdlem4  29721  spthonepeq  29788  clwlkclwwlkflem  30036  clwlkclwwlkfolem  30039  clwlkclwwlkf  30040  clwwisshclwws  30047  clwwlkneq0  30061  3wlkdlem6  30197  eupth2eucrct  30249  eupth2lem1  30250  eupth2lem3lem7  30266  frgr3vlem1  30305  frgr3vlem2  30306  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  numclwwlk5  30420  frgrreg  30426  frgrregord013  30427  friendshipgt3  30430  isgrpo  30529  vciOLD  30593  vcex  30610  nmogtmnf  30802  siilem1  30883  siii  30885  ajmoi  30890  bcsiALT  31211  hhcms  31235  ocval  31312  hsupval  31366  omlsilem  31434  h1de2bi  31586  h1de2ctlem  31587  hosubeq0i  31858  adjmo  31864  nmopgtmnf  31900  nlfnval  31913  nmcopex  32061  nmcfnex  32085  riesz4i  32095  riesz1  32097  riesz2  32098  opsqrlem1  32172  superpos  32386  hatomistici  32394  chpssati  32395  mdsymlem3  32437  an42ds  32479  3o1cs  32490  3o2cs  32491  3o3cs  32492  iunrnmptss  32588  brabgaf  32630  f1mptrn  32654  ffsrn  32743  fpwrelmap  32747  xnn0gt0  32776  hashxpe  32814  prmidl2  33434  mxidlnzrb  33473  evl1deg2  33567  evl1deg3  33568  fedgmul  33644  ordtrest2NEWlem  33868  qqhval2  33928  esumfsup  34034  esumcvg  34050  cntnevol  34192  ddemeas  34200  dya2icoseg2  34243  dya2iocnei  34247  eulerpartlems  34325  eulerpartlemgvv  34341  eulerpart  34347  cndprobprob  34403  ballotlemsdom  34476  ballotth  34502  sgn3da  34506  bnj945  34749  bnj1379  34806  bnj1459  34819  bnj557  34877  bnj571  34882  bnj849  34901  bnj964  34919  bnj978  34925  bnj1018g  34939  bnj1018  34940  bnj1020  34941  bnj1033  34945  bnj1175  34980  bnj1398  35010  bnj1417  35017  bnj1523  35047  nummin  35067  cusgr3cyclex  35104  txpconn  35200  satfv1  35331  satffun  35377  msubco  35499  mclsax  35537  setinds  35742  dfon2lem7  35753  dfon2lem8  35754  pprodss4v  35848  fullfunfv  35911  altxpsspw  35941  funtransport  35995  fvtransport  35996  funray  36104  fvray  36105  funline  36106  fvline  36108  finminlem  36284  bisym1  36385  onsucconni  36403  onsucsuccmpi  36409  weiunse  36434  bj-currypara  36526  axc11n11r  36649  bj-equsal2  36791  bj-xpima1snALT  36923  bj-unexg  37004  bj-bm1.3ii  37030  bj-opelidb1ALT  37132  mptsnunlem  37304  iooelexlt  37328  relowlpssretop  37330  rdgeqoa  37336  difunieq  37340  nlpineqsn  37374  fvineqsneq  37378  wl-lem-nexmo  37521  matunitlindflem1  37576  ptrecube  37580  poimirlem26  37606  poimirlem30  37610  poimir  37613  ismblfin  37621  itg2addnclem  37631  dvasin  37664  sdclem2  37702  totbndbnd  37749  ismgmOLD  37810  exidresid  37839  isrngo  37857  rngoablo2  37869  rngoueqz  37900  isdivrngo  37910  isdrngo1  37916  isdrngo2  37918  ispridl2  37998  relcnveq3  38277  elrelscnveq3  38447  ax12eq  38897  ax12el  38898  lkr0f  39050  hl2at  39362  dalemswapyz  39613  pclfinclN  39907  osumcllem11N  39923  pexmidlem8N  39934  ltrnnid  40093  aks4d1p8  42044  sn-00id  42377  rictr  42475  eu6w  42631  mptfcl  42676  fphpd  42772  elmnc  43093  itgoval  43118  arearect  43176  reabsifpos  43596  clsk3nimkb  44002  grumnud  44255  nanorxor  44274  pm11.71  44366  iotavalsb  44402  sbiota1  44403  2uasbanh  44532  eel0TT  44675  eelT00  44676  eelTTT  44677  eelT11  44678  eelT12  44680  eelTT1  44681  eelT01  44682  eel0T1  44683  eelTT  44742  uunT1p1  44752  uun121  44754  uun121p1  44755  un2122  44761  uunTT1  44764  uunTT1p1  44765  uunTT1p2  44766  uunT11  44767  uunT11p1  44768  uunT11p2  44769  uunT12  44770  uunT12p1  44771  uunT12p2  44772  uunT12p3  44773  uunT12p4  44774  uunT12p5  44775  uun111  44776  3anidm12p2  44778  uun123  44779  3impdirp1  44787  undif3VD  44853  ax6e2ndeqVD  44880  2uasbanhVD  44882  ax6e2ndeqALT  44902  iunconnlem2  44906  sineq0ALT  44908  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem3  45924  stoweidlem17  45938  fourierdlem42  46070  fourierdlem48  46075  fourierdlem50  46077  fourierdlem51  46078  fourierdlem76  46103  fourierdlem83  46110  fourierdlem87  46114  hoidmvval0  46508  rexrsb  47015  2reu8i  47028  2reuimp  47030  afv0nbfvbi  47066  afvfv0bi  47067  afveu  47068  fnbrafvb  47069  afvres  47087  tz6.12-afv  47088  dmfcoafv  47090  afvco2  47091  aovprc  47103  aovrcl  47104  aovmpt4g  47116  afv2eu  47153  afv2res  47154  tz6.12-afv2  47155  tz6.12i-afv2  47158  afv2rnfveq  47177  fvmptrab  47207  fvmptrabdm  47208  fzopred  47237  2ffzoeq  47242  elsprel  47349  prproropf1o  47381  reupr  47396  lighneal  47485  odd2prm2  47592  even3prm2  47593  grictr  47776  grlimgrtrilem2  47819  usgrexmpl12ngric  47853  upgrwlkupwlk  47863  ovn0ssdmfun  47882  islinindfis  48178  rrx2linest  48476  line2ylem  48485  mofeu  48561  isthincd2  48705  setrec2fun  48784  elsetrecslem  48791  setrecsres  48794  secval  48839  cscval  48840  cotval  48841