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  1426  nanass  1510  19.38  1839  19.35  1877  19.8aw  2051  equsexv  2269  sbi2  2302  nfeqf2  2375  equsex  2416  dfmoeu  2529  2mo  2641  axie2  2696  necon1bi  2953  necon1i  2958  r19.35  3088  r19.35OLD  3089  sbhypfOLD  3511  spc2ed  3567  reu6  3697  rabssrabd  4046  uneqin  4252  difin0ss  4336  inelcm  4428  rzal  4472  ralf0  4477  falseral0  4479  raaan2  4484  difprsn1  4764  tppreqb  4769  n0snor2el  4797  unissint  4936  intminss  4938  dfiun2g  4994  iununi  5063  triin  5231  bm1.3iiOLD  5257  eusv2nf  5350  reusv3i  5359  moabex  5419  opelopabt  5492  eqrelrel  5760  opeliunxp2  5802  opelrn  5907  ssxpb  6147  xpima  6155  xpimasn  6158  dmsn0el  6184  relcnvtr  6240  relcoi2  6250  elsnxp  6264  reuop  6266  iotanul  6489  f1imadifssran  6602  dffv2  6956  fnfvrnss  7093  fressnfv  7132  fconst5  7180  f1mpt  7236  isocnv3  7307  f1owe  7328  ovprc  7425  fvmpopr2d  7551  onminesb  7769  onminsb  7770  onintrab  7772  onnminsb  7775  ordsuci  7784  onsucuni2  7809  tfindsg2  7838  zfrep6  7933  fo1stres  7994  fo2ndres  7995  bropopvvv  8069  bropfvvvv  8071  frxp  8105  poseq  8137  soseq  8138  opeliunxp2f  8189  mpoxopoveqd  8200  reldmtpos  8213  frrlem4  8268  tfrlem5  8348  tfrlem9  8353  tfr2  8366  rdgsuc  8392  oaordi  8510  oeordi  8551  omopthi  8625  on2recsov  8632  fvmptmap  8854  mptelixpg  8908  ener  8972  domtr  8978  snfiOLD  9015  unen  9017  undom  9029  dom0  9069  xpf1o  9103  mapen  9105  rexdif1enOLD  9123  dif1enOLD  9126  pssnn  9132  unfi  9135  ssfi  9137  ensymfib  9148  entrfil  9149  enfii  9150  domtrfil  9156  unxpdomlem3  9199  isinf  9207  isinfOLD  9208  frfi  9232  unblem1  9239  fofinf1o  9283  fsuppun  9338  inf3lem2  9582  inf3lem5  9585  cantnfp1lem1  9631  cantnfp1lem3  9633  tcmin  9694  frr2  9713  r1ordg  9731  r1ord  9733  rankr1ai  9751  r1val3  9791  bndrank  9794  unbndrank  9795  rankr1b  9817  rankxplim3  9834  tcrank  9837  xpnum  9904  cardmin2  9952  infxpenlem  9966  fseqen  9980  dfac8clem  9985  alephsson  10053  alephfp  10061  dfac4  10075  kmlem6  10109  kmlem8  10111  kmlem9  10112  cflem  10198  infpssr  10261  fin1a2lem12  10364  axcc4  10392  axcc4dom  10394  ac6s2  10439  zornn0g  10458  cardidg  10501  unsnen  10506  pwcfsdom  10536  cfpwsdom  10537  gchpwdom  10623  r1tskina  10735  intgru  10767  indpi  10860  nqereu  10882  supsrlem  11064  letrii  11299  dfnn3  12200  zaddcl  12573  nn0ind  12629  fnn0ind  12633  ublbneg  12892  nn01to3  12900  infmrp1  13305  fz0  13500  fzo1fzo0n0  13676  elfzom1elp1fzo  13693  fzo0end  13719  elfznelfzo  13733  fzind2  13746  injresinjlem  13748  fleqceilz  13816  nnsinds  13953  nn0sinds  13954  faclbnd4lem1  14258  hashinf  14300  hasheqf1oi  14316  hashgt0elex  14366  hashgt23el  14389  hashfacen  14419  hash2prde  14435  hash2sspr  14454  fun2dmnop0  14469  iswrddm0  14503  swrdnnn0nd  14621  swrdnd0  14622  swrdlsw  14632  pfxn0  14651  pfxnd0  14653  swrdswrdlem  14669  pfxccatin12lem3  14697  pfxccat3  14699  pfxccat3a  14703  swrdccat3blem  14704  cshwsublen  14761  cshwidxmod  14768  repswcshw  14777  cshw1  14787  trclun  14980  dmtrclfv  14984  rediv  15097  imdiv  15104  fsump1i  15735  modfsummods  15759  bpolydiflem  16020  bpoly3  16024  bpoly4  16025  cos1bnd  16155  sinltx  16157  rpnnen2lem1  16182  rpnnen2lem2  16183  rpnnen2lem12  16193  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  gcdcllem1  16469  gcdaddmlem  16494  dfgcd2  16516  algfx  16550  lcmledvds  16569  lcmfunsnlem  16611  lcmfun  16615  coprmprod  16631  coprmproddvdslem  16632  odzval  16762  odzdvds  16766  prmreclem5  16891  mul4sq  16925  prmgaplem5  17026  prmgaplem6  17027  imasaddfnlem  17491  mreexexlem4d  17608  joindmss  18338  meetdmss  18352  gictr  19208  cntzval  19253  symg2bas  19323  odfval  19462  efgsfo  19669  efgrelexlemb  19680  dprddomcld  19933  dprdsubg  19956  dprd2da  19974  lssacs  20873  cnfldinv  21314  pzriprnglem7  21397  ocvval  21576  selvval  22022  dmatmul  22384  mdetfval1  22477  mndifsplit  22523  fvmptnn04if  22736  toprntopon  22812  opnnei  23007  ordtbas2  23078  ordtrest2lem  23090  lmmo  23267  fincmp  23280  bwth  23297  txbas  23454  ptcnplem  23508  tx2ndc  23538  hmphtr  23670  fbun  23727  filconn  23770  ptcmplem5  23943  cnextcn  23954  utoptop  24122  ucncn  24172  metust  24446  cfilucfil  24447  elcncf1di  24788  xrhmeo  24844  phtpycc  24890  copco  24918  pcohtpylem  24919  pcopt  24922  pcopt2  24923  ncvsi  25051  ovolval  25374  iunmbl2  25458  itg2splitlem  25649  cpnfval  25834  plyval  26098  fta1  26216  aaliou2b  26249  tayl0  26269  ulmdvlem3  26311  radcnvlem2  26323  dvradcnv  26330  reeff1o  26357  sincosq1lem  26406  sincosq2sgn  26408  sincosq4sgn  26410  sinq12ge0  26417  logrncl  26476  eflog  26485  cxpge0  26592  logb1  26679  atanf  26790  atanbnd  26836  igamf  26961  igamcl  26962  lgsne0  27246  mul2sq  27330  2sqreultblem  27359  pntibnd  27504  ostth  27550  nocvxminlem  27689  nocvxmin  27690  cutlt  27840  norec2ov  27864  addsuniflem  27908  mulsuniflem  28052  zmulscld  28285  zseo  28308  mptelee  28822  axlowdimlem9  28877  axlowdimlem12  28880  axcontlem2  28892  axcontlem12  28902  structgrssvtx  28951  structgrssiedg  28952  lpvtx  28995  nbuhgr  29270  nbumgr  29274  nbuhgr2vtx1edgblem  29278  nbgr0edglem  29283  nbgr1vtx  29285  uvtx01vtx  29324  prcliscplgr  29341  cusgrsizeinds  29380  sizusglecusglem2  29390  uhgrvd00  29462  fusgrregdegfi  29497  rusgr1vtxlem  29515  wlkeq  29562  wlk1walk  29567  uspgr2wlkeq  29574  wlklenvclwlk  29583  wlkreslem  29597  wlkdlem2  29611  wlkdlem4  29613  spthonepeq  29682  cyclnumvtx  29730  clwlkclwwlkflem  29933  clwlkclwwlkfolem  29936  clwlkclwwlkf  29937  clwwisshclwws  29944  clwwlkneq0  29958  3wlkdlem6  30094  eupth2eucrct  30146  eupth2lem1  30147  eupth2lem3lem7  30163  frgr3vlem1  30202  frgr3vlem2  30203  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  numclwwlk5  30317  frgrreg  30323  frgrregord013  30324  friendshipgt3  30327  isgrpo  30426  vciOLD  30490  vcex  30507  nmogtmnf  30699  siilem1  30780  siii  30782  ajmoi  30787  bcsiALT  31108  hhcms  31132  ocval  31209  hsupval  31263  omlsilem  31331  h1de2bi  31483  h1de2ctlem  31484  hosubeq0i  31755  adjmo  31761  nmopgtmnf  31797  nlfnval  31810  nmcopex  31958  nmcfnex  31982  riesz4i  31992  riesz1  31994  riesz2  31995  opsqrlem1  32069  superpos  32283  hatomistici  32291  chpssati  32292  mdsymlem3  32334  an42ds  32379  3o1cs  32390  3o2cs  32391  3o3cs  32392  iunrnmptss  32494  brabgaf  32536  f1mptrn  32559  ffsrn  32652  fpwrelmap  32656  xnn0gt0  32692  hashxpe  32732  sgn3da  32759  elrgspnlem4  33196  prmidl2  33412  mxidlnzrb  33451  evl1deg2  33546  evl1deg3  33547  fedgmul  33627  cos9thpiminplylem2  33773  ordtrest2NEWlem  33912  qqhval2  33972  esumfsup  34060  esumcvg  34076  cntnevol  34218  ddemeas  34226  dya2icoseg2  34269  dya2iocnei  34273  eulerpartlems  34351  eulerpartlemgvv  34367  eulerpart  34373  cndprobprob  34429  ballotlemsdom  34503  ballotth  34529  bnj945  34763  bnj1379  34820  bnj1459  34833  bnj557  34891  bnj571  34896  bnj849  34915  bnj964  34933  bnj978  34939  bnj1018g  34953  bnj1018  34954  bnj1020  34955  bnj1033  34959  bnj1175  34994  bnj1398  35024  bnj1417  35031  bnj1523  35061  nummin  35081  onvf1odlem4  35093  onvf1od  35094  cusgr3cyclex  35123  txpconn  35219  satfv1  35350  satffun  35396  msubco  35518  mclsax  35556  setinds  35766  dfon2lem7  35777  dfon2lem8  35778  pprodss4v  35872  fullfunfv  35935  altxpsspw  35965  funtransport  36019  fvtransport  36020  funray  36128  fvray  36129  funline  36130  fvline  36132  finminlem  36306  bisym1  36407  onsucconni  36425  onsucsuccmpi  36431  weiunse  36456  bj-currypara  36548  axc11n11r  36671  bj-equsal2  36813  bj-xpima1snALT  36945  bj-unexg  37026  bj-bm1.3ii  37052  bj-opelidb1ALT  37154  mptsnunlem  37326  iooelexlt  37350  relowlpssretop  37352  rdgeqoa  37358  difunieq  37362  nlpineqsn  37396  fvineqsneq  37400  wl-ax12v2cl  37494  wl-lem-nexmo  37555  matunitlindflem1  37610  ptrecube  37614  poimirlem26  37640  poimirlem30  37644  poimir  37647  ismblfin  37655  itg2addnclem  37665  dvasin  37698  sdclem2  37736  totbndbnd  37783  ismgmOLD  37844  exidresid  37873  isrngo  37891  rngoablo2  37903  rngoueqz  37934  isdivrngo  37944  isdrngo1  37950  isdrngo2  37952  ispridl2  38032  relcnveq3  38309  elrelscnveq3  38482  dmqsblocks  38845  ax12eq  38934  ax12el  38935  lkr0f  39087  hl2at  39399  dalemswapyz  39650  pclfinclN  39944  osumcllem11N  39960  pexmidlem8N  39971  ltrnnid  40130  aks4d1p8  42075  redvmptabs  42348  sn-00id  42389  rictr  42508  eu6w  42664  mptfcl  42708  fphpd  42804  elmnc  43125  itgoval  43150  arearect  43204  reabsifpos  43623  clsk3nimkb  44029  grumnud  44275  nanorxor  44294  pm11.71  44386  iotavalsb  44422  sbiota1  44423  2uasbanh  44551  eel0TT  44693  eelT00  44694  eelTTT  44695  eelT11  44696  eelT12  44698  eelTT1  44699  eelT01  44700  eel0T1  44701  eelTT  44760  uunT1p1  44770  uun121  44772  uun121p1  44773  un2122  44779  uunTT1  44782  uunTT1p1  44783  uunTT1p2  44784  uunT11  44785  uunT11p1  44786  uunT11p2  44787  uunT12  44788  uunT12p1  44789  uunT12p2  44790  uunT12p3  44791  uunT12p4  44792  uunT12p5  44793  uun111  44794  3anidm12p2  44796  uun123  44797  3impdirp1  44805  undif3VD  44871  ax6e2ndeqVD  44898  2uasbanhVD  44900  ax6e2ndeqALT  44920  iunconnlem2  44924  sineq0ALT  44926  modelaxreplem1  44968  permaxrep  44996  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem3  46001  stoweidlem17  46015  fourierdlem42  46147  fourierdlem48  46152  fourierdlem50  46154  fourierdlem51  46155  fourierdlem76  46180  fourierdlem83  46187  fourierdlem87  46191  hoidmvval0  46585  evenwodadd  46886  rexrsb  47101  2reu8i  47114  2reuimp  47116  afv0nbfvbi  47152  afvfv0bi  47153  afveu  47154  fnbrafvb  47155  afvres  47173  tz6.12-afv  47174  dmfcoafv  47176  afvco2  47177  aovprc  47189  aovrcl  47190  aovmpt4g  47202  afv2eu  47239  afv2res  47240  tz6.12-afv2  47241  tz6.12i-afv2  47244  afv2rnfveq  47263  fvmptrab  47293  fvmptrabdm  47294  fzopred  47323  2ffzoeq  47328  elsprel  47476  prproropf1o  47508  reupr  47523  lighneal  47612  odd2prm2  47719  even3prm2  47720  grictr  47923  grlimgrtrilem2  47994  usgrexmpl12ngric  48029  gpgprismgr4cycllem8  48092  gpgprismgr4cycllem11  48095  pgnbgreunbgrlem2lem1  48104  upgrwlkupwlk  48128  ovn0ssdmfun  48147  islinindfis  48438  rrx2linest  48731  line2ylem  48740  mofeu  48836  homf0  48998  uobffth  49207  uobeqw  49208  initopropd  49232  termopropd  49233  zeroopropd  49234  fucofvalne  49314  isthincd2  49426  lanrcl  49610  ranrcl  49611  setrec2fun  49681  elsetrecslem  49688  setrecsres  49691  secval  49736  cscval  49737  cotval  49738