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  1119  3ori  1427  an42ds  1492  nanass  1512  19.38  1841  19.35  1879  19.8aw  2054  equsexv  2276  sbi2  2309  nfeqf2  2382  equsex  2423  dfmoeu  2536  2mo  2649  axie2  2704  necon1bi  2961  necon1i  2966  r19.35  3096  spc2ed  3557  reu6  3686  rabssrabd  4037  uneqin  4243  difin0ss  4327  inelcm  4419  falseral0OLD  4470  raaan2  4477  difprsn1  4758  tppreqb  4763  n0snor2el  4791  unissint  4929  intminss  4931  dfiun2g  4987  iununi  5056  triin  5223  bm1.3iiOLD  5249  eusv2nf  5342  reusv3i  5351  axprglem  5382  axprg  5383  moabexOLD  5414  opelopabt  5488  eqrelrel  5754  opeliunxp2  5795  opelrn  5900  ssxpb  6140  xpima  6148  xpimasn  6151  dmsn0el  6177  relcnvtr  6234  relcoi2  6243  elsnxp  6257  reuop  6259  iotanul  6480  f1imadifssran  6586  dffv2  6937  fnfvrnss  7075  fressnfv  7115  fconst5  7162  f1mpt  7217  isocnv3  7288  f1owe  7309  ovprc  7406  fvmpopr2d  7530  onminesb  7748  onminsb  7749  onintrab  7751  onnminsb  7754  ordsuci  7763  onsucuni2  7786  tfindsg2  7814  zfrep6  7909  fo1stres  7969  fo2ndres  7970  bropopvvv  8042  bropfvvvv  8044  frxp  8078  poseq  8110  soseq  8111  opeliunxp2f  8162  mpoxopoveqd  8173  reldmtpos  8186  frrlem4  8241  tfrlem5  8321  tfrlem9  8326  tfr2  8339  rdgsuc  8365  oaordi  8483  oeordi  8525  omopthi  8599  on2recsov  8606  fvmptmap  8831  mptelixpg  8885  ener  8950  domtr  8956  unen  8994  undom  9005  dom0  9045  xpf1o  9079  mapen  9081  pssnn  9105  unfi  9107  ssfi  9109  ensymfib  9120  entrfil  9121  enfii  9122  domtrfil  9128  unxpdomlem3  9170  isinf  9177  frfi  9197  unblem1  9204  fofinf1o  9244  fsuppun  9302  elirrv  9514  inf3lem2  9550  inf3lem5  9553  cantnfp1lem1  9599  cantnfp1lem3  9601  tcmin  9660  setinds  9670  frr2  9684  r1ordg  9702  r1ord  9704  rankr1ai  9722  r1val3  9762  bndrank  9765  unbndrank  9766  rankr1b  9788  rankxplim3  9805  tcrank  9808  xpnum  9875  cardmin2  9923  infxpenlem  9935  fseqen  9949  dfac8clem  9954  alephsson  10022  alephfp  10030  dfac4  10044  kmlem6  10078  kmlem8  10080  kmlem9  10081  cflem  10167  infpssr  10230  fin1a2lem12  10333  axcc4  10361  axcc4dom  10363  ac6s2  10408  zornn0g  10427  cardidg  10470  unsnen  10475  pwcfsdom  10506  cfpwsdom  10507  gchpwdom  10593  r1tskina  10705  intgru  10737  indpi  10830  nqereu  10852  supsrlem  11034  letrii  11270  dfnn3  12171  zaddcl  12543  nn0ind  12599  fnn0ind  12603  ublbneg  12858  nn01to3  12866  infmrp1  13272  fz0  13467  fzo1fzo0n0  13643  elfzom1elp1fzo  13660  fzo0end  13686  elfznelfzo  13701  fzind2  13716  injresinjlem  13718  fleqceilz  13786  nnsinds  13923  nn0sinds  13924  faclbnd4lem1  14228  hashinf  14270  hasheqf1oi  14286  hashgt0elex  14336  hashgt23el  14359  hashfacen  14389  hash2prde  14405  hash2sspr  14424  fun2dmnop0  14439  iswrddm0  14473  swrdnnn0nd  14592  swrdnd0  14593  swrdlsw  14603  pfxn0  14622  pfxnd0  14624  swrdswrdlem  14639  pfxccatin12lem3  14667  pfxccat3  14669  pfxccat3a  14673  swrdccat3blem  14674  cshwsublen  14731  cshwidxmod  14738  repswcshw  14747  cshw1  14757  trclun  14949  dmtrclfv  14953  rediv  15066  imdiv  15073  fsump1i  15704  modfsummods  15728  bpolydiflem  15989  bpoly3  15993  bpoly4  15994  cos1bnd  16124  sinltx  16126  rpnnen2lem1  16151  rpnnen2lem2  16152  rpnnen2lem12  16162  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  gcdcllem1  16438  gcdaddmlem  16463  dfgcd2  16485  algfx  16519  lcmledvds  16538  lcmfunsnlem  16580  lcmfun  16584  coprmprod  16600  coprmproddvdslem  16601  odzval  16731  odzdvds  16735  prmreclem5  16860  mul4sq  16894  prmgaplem5  16995  prmgaplem6  16996  imasaddfnlem  17461  mreexexlem4d  17582  joindmss  18312  meetdmss  18326  gictr  19217  cntzval  19262  symg2bas  19334  odfval  19473  efgsfo  19680  efgrelexlemb  19691  dprddomcld  19944  dprdsubg  19967  dprd2da  19985  lssacs  20930  cnfldinv  21369  pzriprnglem7  21454  ocvval  21634  selvval  22090  dmatmul  22453  mdetfval1  22546  mndifsplit  22592  fvmptnn04if  22805  toprntopon  22881  opnnei  23076  ordtbas2  23147  ordtrest2lem  23159  lmmo  23336  fincmp  23349  bwth  23366  txbas  23523  ptcnplem  23577  tx2ndc  23607  hmphtr  23739  fbun  23796  filconn  23839  ptcmplem5  24012  cnextcn  24023  utoptop  24190  ucncn  24240  metust  24514  cfilucfil  24515  elcncf1di  24856  xrhmeo  24912  phtpycc  24958  copco  24986  pcohtpylem  24987  pcopt  24990  pcopt2  24991  ncvsi  25119  ovolval  25442  iunmbl2  25526  itg2splitlem  25717  cpnfval  25902  plyval  26166  fta1  26284  aaliou2b  26317  tayl0  26337  ulmdvlem3  26379  radcnvlem2  26391  dvradcnv  26398  reeff1o  26425  sincosq1lem  26474  sincosq2sgn  26476  sincosq4sgn  26478  sinq12ge0  26485  logrncl  26544  eflog  26553  cxpge0  26660  logb1  26747  atanf  26858  atanbnd  26904  igamf  27029  igamcl  27030  lgsne0  27314  mul2sq  27398  2sqreultblem  27427  pntibnd  27572  ostth  27618  nobdaymin  27761  nocvxminlem  27762  cutlt  27940  norec2ov  27965  addsuniflem  28009  mulsuniflem  28157  oldfib  28385  zmulscld  28405  zseo  28430  z12addscl  28485  mpteleeOLD  28980  axlowdimlem9  29035  axlowdimlem12  29038  axcontlem2  29050  axcontlem12  29060  structgrssvtx  29109  structgrssiedg  29110  lpvtx  29153  nbuhgr  29428  nbumgr  29432  nbuhgr2vtx1edgblem  29436  nbgr0edglem  29441  nbgr1vtx  29443  uvtx01vtx  29482  prcliscplgr  29499  cusgrsizeinds  29538  sizusglecusglem2  29548  uhgrvd00  29620  fusgrregdegfi  29655  rusgr1vtxlem  29673  wlkeq  29719  wlk1walk  29724  uspgr2wlkeq  29731  wlklenvclwlk  29739  wlkreslem  29753  wlkdlem2  29767  wlkdlem4  29769  spthonepeq  29837  cyclnumvtx  29885  clwlkclwwlkflem  30091  clwlkclwwlkfolem  30094  clwlkclwwlkf  30095  clwwisshclwws  30102  clwwlkneq0  30116  3wlkdlem6  30252  eupth2eucrct  30304  eupth2lem1  30305  eupth2lem3lem7  30321  frgr3vlem1  30360  frgr3vlem2  30361  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  numclwwlk5  30475  frgrreg  30481  frgrregord013  30482  friendshipgt3  30485  isgrpo  30585  vciOLD  30649  vcex  30666  nmogtmnf  30858  siilem1  30939  siii  30941  ajmoi  30946  bcsiALT  31267  hhcms  31291  ocval  31368  hsupval  31422  omlsilem  31490  h1de2bi  31642  h1de2ctlem  31643  hosubeq0i  31914  adjmo  31920  nmopgtmnf  31956  nlfnval  31969  nmcopex  32117  nmcfnex  32141  riesz4i  32151  riesz1  32153  riesz2  32154  opsqrlem1  32228  superpos  32442  hatomistici  32450  chpssati  32451  mdsymlem3  32493  3o1cs  32547  3o2cs  32548  3o3cs  32549  iunrnmptss  32652  brabgaf  32696  f1mptrn  32725  ffsrn  32818  xnn0gt0  32860  hashxpe  32898  sgn3da  32926  elrgspnlem4  33339  prmidl2  33534  mxidlnzrb  33573  evl1deg2  33670  evl1deg3  33671  fedgmul  33809  cos9thpiminplylem2  33961  ordtrest2NEWlem  34100  qqhval2  34160  esumfsup  34248  esumcvg  34264  cntnevol  34406  ddemeas  34414  dya2icoseg2  34456  dya2iocnei  34460  eulerpartlems  34538  eulerpartlemgvv  34554  eulerpart  34560  cndprobprob  34616  ballotlemsdom  34690  ballotth  34716  bnj945  34950  bnj1379  35006  bnj1459  35019  bnj557  35077  bnj571  35082  bnj849  35101  bnj964  35119  bnj978  35125  bnj1018g  35139  bnj1018  35140  bnj1020  35141  bnj1033  35145  bnj1175  35180  bnj1398  35210  bnj1417  35217  bnj1523  35247  nummin  35270  r1omhf  35283  axprALT2  35287  fineqvnttrclselem1  35299  onvf1odlem4  35322  onvf1od  35323  cusgr3cyclex  35352  txpconn  35448  satfv1  35579  satffun  35625  msubco  35747  mclsax  35785  dfon2lem7  36003  dfon2lem8  36004  pprodss4v  36098  fullfunfv  36163  altxpsspw  36193  funtransport  36247  fvtransport  36248  funray  36356  fvray  36357  funline  36358  fvline  36360  finminlem  36534  bisym1  36635  onsucconni  36653  onsucsuccmpi  36659  weiunse  36684  bj-currypara  36784  bj-cbvaw  36884  axc11n11r  36928  bj-equsal2  37073  bj-xpima1snALT  37205  bj-unexg  37286  bj-bm1.3ii  37312  bj-axseprep  37322  bj-axreprepsep  37323  bj-opelidb1ALT  37421  mptsnunlem  37593  iooelexlt  37617  relowlpssretop  37619  rdgeqoa  37625  difunieq  37629  nlpineqsn  37663  fvineqsneq  37667  wl-ax12v2cl  37761  wl-lem-nexmo  37822  matunitlindflem1  37867  ptrecube  37871  poimirlem26  37897  poimirlem30  37901  poimir  37904  ismblfin  37912  itg2addnclem  37922  dvasin  37955  sdclem2  37993  totbndbnd  38040  ismgmOLD  38101  exidresid  38130  isrngo  38148  rngoablo2  38160  rngoueqz  38191  isdivrngo  38201  isdrngo1  38207  isdrngo2  38209  ispridl2  38289  relcnveq3  38578  elrelscnveq3  38878  disjimeceqim  39055  dmqsblocks  39218  ax12eq  39317  ax12el  39318  lkr0f  39470  hl2at  39781  dalemswapyz  40032  pclfinclN  40326  osumcllem11N  40342  pexmidlem8N  40353  ltrnnid  40512  aks4d1p8  42457  redvmptabs  42730  sn-00id  42771  rictr  42890  eu6w  43034  mptfcl  43077  fphpd  43173  elmnc  43493  itgoval  43518  arearect  43572  reabsifpos  43990  clsk3nimkb  44396  grumnud  44642  nanorxor  44661  pm11.71  44753  iotavalsb  44789  sbiota1  44790  2uasbanh  44917  eel0TT  45059  eelT00  45060  eelTTT  45061  eelT11  45062  eelT12  45064  eelTT1  45065  eelT01  45066  eel0T1  45067  eelTT  45126  uunT1p1  45136  uun121  45138  uun121p1  45139  un2122  45145  uunTT1  45148  uunTT1p1  45149  uunTT1p2  45150  uunT11  45151  uunT11p1  45152  uunT11p2  45153  uunT12  45154  uunT12p1  45155  uunT12p2  45156  uunT12p3  45157  uunT12p4  45158  uunT12p5  45159  uun111  45160  3anidm12p2  45162  uun123  45163  3impdirp1  45171  undif3VD  45237  ax6e2ndeqVD  45264  2uasbanhVD  45266  ax6e2ndeqALT  45286  iunconnlem2  45290  sineq0ALT  45292  modelaxreplem1  45334  permaxrep  45362  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  stoweidlem3  46361  stoweidlem17  46375  fourierdlem42  46507  fourierdlem48  46512  fourierdlem50  46514  fourierdlem51  46515  fourierdlem76  46540  fourierdlem83  46547  fourierdlem87  46551  hoidmvval0  46945  evenwodadd  47245  rexrsb  47460  2reu8i  47473  2reuimp  47475  afv0nbfvbi  47511  afvfv0bi  47512  afveu  47513  fnbrafvb  47514  afvres  47532  tz6.12-afv  47533  dmfcoafv  47535  afvco2  47536  aovprc  47548  aovrcl  47549  aovmpt4g  47561  afv2eu  47598  afv2res  47599  tz6.12-afv2  47600  tz6.12i-afv2  47603  afv2rnfveq  47622  fvmptrab  47652  fvmptrabdm  47653  fzopred  47682  2ffzoeq  47687  elsprel  47835  prproropf1o  47867  reupr  47882  lighneal  47971  odd2prm2  48078  even3prm2  48079  grictr  48283  grlimgrtrilem2  48362  usgrexmpl12ngric  48398  gpgprismgr4cycllem8  48462  gpgprismgr4cycllem11  48465  pgnbgreunbgrlem2lem1  48474  upgrwlkupwlk  48500  ovn0ssdmfun  48519  islinindfis  48809  rrx2linest  49102  line2ylem  49111  mofeu  49207  homf0  49368  uobffth  49577  uobeqw  49578  initopropd  49602  termopropd  49603  zeroopropd  49604  fucofvalne  49684  isthincd2  49796  lanrcl  49980  ranrcl  49981  setrec2fun  50051  elsetrecslem  50058  setrecsres  50061  secval  50106  cscval  50107  cotval  50108