Theorem sylbir 237

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3i  293  ex  416  3expa  1131  3ori  1443  an42ds  1510  nanass  1530  19.38  1859  19.35  1897  19.8aw  2072  sbrimvw  2124  equsexv  2303  sbi2  2336  nfeqf2  2408  equsex  2449  dfmoeu  2562  2mo  2675  axie2  2729  necon1bi  2985  necon1i  2990  r19.35  3120  spc2ed  3560  reu6  3689  rabssrabd  4036  uneqin  4241  difin0ss  4326  inelcm  4419  falseral0OLD  4469  raaan2  4476  difprsn1  4760  tppreqb  4765  n0snor2el  4791  unissint  4930  intminss  4932  dfiun2g  4987  iununi  5056  triin  5224  bm1.3iiOLD  5252  eusv2nf  5352  reusv3i  5361  axprglem  5393  axprg  5394  moabexOLD  5426  opelopabt  5502  eqrelrel  5769  opeliunxp2  5810  opelrn  5919  ssxpb  6160  xpima  6168  xpimasn  6171  dmsn0el  6198  relcnvtr  6255  relcoi2  6264  elsnxp  6278  reuop  6280  iotanul  6501  f1imadifssran  6607  dffv2  6962  fnfvrnss  7102  fressnfv  7143  fconst5  7190  f1mpt  7245  isocnv3  7316  f1owe  7337  ovprc  7434  fvmpopr2d  7558  onminesb  7776  onminsb  7777  onintrab  7779  onnminsb  7782  ordsuci  7791  onsucuni2  7814  tfindsg2  7842  zfrep6OLD  7936  fo1stres  7996  fo2ndres  7997  bropopvvv  8069  bropfvvvv  8071  frxp  8106  poseq  8138  soseq  8139  opeliunxp2f  8190  mpoxopoveqd  8201  reldmtpos  8214  frrlem4  8270  tfrlem5  8350  tfrlem9  8356  tfr2  8369  rdgsuc  8395  oaordi  8515  oeordi  8557  omopthi  8631  on2recsov  8638  fvmptmap  8863  mptelixpg  8917  ener  8982  domtr  8988  unen  9026  undom  9037  dom0  9077  xpf1o  9111  mapen  9113  pssnn  9137  unfi  9139  ssfi  9141  ensymfib  9152  entrfil  9153  enfii  9154  domtrfil  9160  unxpdomlem3  9202  isinf  9209  frfi  9229  unblem1  9236  fofinf1o  9275  fsuppun  9333  elirrvOLD  9546  inf3lem2  9584  inf3lem5  9587  cantnfp1lem1  9633  cantnfp1lem3  9635  tcmin  9694  setinds  9704  frr2  9718  r1ordg  9736  r1ord  9738  rankr1ai  9756  r1val3  9796  bndrank  9799  unbndrank  9800  rankr1b  9822  rankxplim3  9839  tcrank  9842  xpnum  9909  cardmin2  9957  infxpenlem  9969  fseqen  9983  dfac8clem  9988  alephsson  10056  alephfp  10064  dfac4  10078  kmlem6  10112  kmlem8  10114  kmlem9  10115  cflem  10201  infpssr  10265  fin1a2lem12  10368  axcc4  10396  axcc4dom  10398  ac6s2  10443  zornn0g  10462  cardidg  10505  unsnen  10510  pwcfsdom  10541  cfpwsdom  10542  gchpwdom  10628  r1tskina  10740  intgru  10772  indpi  10865  nqereu  10887  supsrlem  11069  letrii  11308  dfnn3  12224  zaddcl  12611  nn0ind  12668  fnn0ind  12672  ublbneg  12934  nn01to3  12942  infmrp1  13348  fz0  13544  fzo1fzo0n0  13721  elfzom1elp1fzo  13738  fzo0end  13764  elfznelfzo  13779  fzind2  13794  injresinjlem  13796  fleqceilz  13864  nnsinds  14001  nn0sinds  14002  faclbnd4lem1  14306  hashinf  14348  hasheqf1oi  14364  hashgt0elex  14414  hashgt23el  14437  hashfacen  14467  hash2prde  14483  hash2sspr  14502  fun2dmnop0  14517  iswrddm0  14551  swrdnnn0nd  14670  swrdnd0  14671  swrdlsw  14681  pfxn0  14700  pfxnd0  14702  swrdswrdlem  14717  pfxccatin12lem3  14745  pfxccat3  14747  pfxccat3a  14751  swrdccat3blem  14752  cshwsublen  14809  cshwidxmod  14816  repswcshw  14825  cshw1  14835  trclun  15027  dmtrclfv  15031  sgn3da  15114  rediv  15158  imdiv  15165  fsump1i  15796  modfsummods  15821  bpolydiflem  16084  bpoly3  16088  bpoly4  16089  cos1bnd  16219  sinltx  16221  rpnnen2lem1  16246  rpnnen2lem2  16247  rpnnen2lem12  16257  odd2np1  16375  opoe  16397  omoe  16398  opeo  16399  omeo  16400  gcdcllem1  16533  gcdaddmlem  16558  dfgcd2  16580  algfx  16614  lcmledvds  16633  lcmfunsnlem  16675  lcmfun  16679  coprmprod  16695  coprmproddvdslem  16696  odzval  16827  odzdvds  16831  prmreclem5  16956  mul4sq  16990  prmgaplem5  17091  prmgaplem6  17092  imasaddfnlem  17558  mreexexlem4d  17679  joindmss  18409  meetdmss  18423  gictr  19316  cntzval  19361  symg2bas  19433  odfval  19572  efgsfo  19779  efgrelexlemb  19790  dprddomcld  20043  dprdsubg  20066  dprd2da  20084  lssacs  21034  cnfldinv  21455  pzriprnglem7  21539  ocvval  21719  selvval  22173  dmatmul  22557  mdetfval1  22650  mndifsplit  22696  fvmptnn04if  22909  toprntopon  22985  opnnei  23180  ordtbas2  23251  ordtrest2lem  23263  lmmo  23440  fincmp  23453  bwth  23470  txbas  23627  ptcnplem  23681  tx2ndc  23711  hmphtr  23843  fbun  23900  filconn  23943  ptcmplem5  24116  cnextcn  24127  utoptop  24294  ucncn  24344  metust  24618  cfilucfil  24619  elcncf1di  24957  xrhmeo  25008  phtpycc  25053  copco  25080  pcohtpylem  25081  pcopt  25084  pcopt2  25085  ncvsi  25213  ovolval  25535  iunmbl2  25619  itg2splitlem  25810  cpnfval  25994  plyval  26253  fta1  26372  aaliou2b  26405  tayl0  26425  ulmdvlem3  26465  radcnvlem2  26477  dvradcnv  26484  reeff1o  26510  sincosq1lem  26562  sincosq2sgn  26564  sincosq4sgn  26566  sinq12ge0  26573  logrncl  26632  eflog  26641  cxpge0  26748  logb1  26834  atanf  26945  atanbnd  26991  igamf  27115  igamcl  27116  lgsne0  27399  mul2sq  27483  2sqreultblem  27512  pntibnd  27657  ostth  27703  nobdaymin  27846  nocvxminlem  27847  cutlt  28025  norec2ov  28050  addsuniflem  28094  mulsuniflem  28242  oldfib  28470  zmulscld  28490  zseo  28515  z12addscl  28570  mpteleeOLD  29096  axlowdimlem9  29151  axlowdimlem12  29154  axcontlem2  29166  axcontlem12  29176  structgrssvtx  29225  structgrssiedg  29226  lpvtx  29269  nbuhgr  29544  nbumgr  29548  nbuhgr2vtx1edgblem  29552  nbgr0edglem  29557  nbgr1vtx  29559  uvtx01vtx  29598  prcliscplgr  29615  cusgrsizeinds  29653  sizusglecusglem2  29663  uhgrvd00  29735  fusgrregdegfi  29770  rusgr1vtxlem  29788  wlkeq  29834  wlk1walk  29839  uspgr2wlkeq  29846  wlklenvclwlk  29854  wlkreslem  29868  wlkdlem2  29882  wlkdlem4  29884  spthonepeq  29952  cyclnumvtx  30000  clwlkclwwlkflem  30206  clwlkclwwlkfolem  30209  clwlkclwwlkf  30210  clwwisshclwws  30217  clwwlkneq0  30231  3wlkdlem6  30367  eupth2eucrct  30419  eupth2lem1  30420  eupth2lem3lem7  30436  frgr3vlem1  30475  frgr3vlem2  30476  frgrncvvdeqlem8  30508  frgrncvvdeqlem9  30509  numclwwlk5  30590  frgrreg  30596  frgrregord013  30597  friendshipgt3  30600  isgrpo  30700  vciOLD  30764  vcex  30781  nmogtmnf  30973  siilem1  31054  siii  31056  ajmoi  31061  bcsiALT  31382  hhcms  31406  ocval  31483  hsupval  31537  omlsilem  31605  h1de2bi  31757  h1de2ctlem  31758  hosubeq0i  32029  adjmo  32035  nmopgtmnf  32071  nlfnval  32084  nmcopex  32232  nmcfnex  32256  riesz4i  32266  riesz1  32268  riesz2  32269  opsqrlem1  32343  superpos  32557  hatomistici  32565  chpssati  32566  mdsymlem3  32608  3o1cs  32661  3o2cs  32662  3o3cs  32663  iunrnmptss  32765  brabgaf  32808  f1mptrn  32837  ffsrn  32930  xnn0gt0  32971  hashxpe  33009  elrgspnlem4  33426  prmidl2  33627  mxidlnzrb  33668  evl1deg2  33773  evl1deg3  33774  fedgmul  33928  cos9thpiminplylem2  34080  ordtrest2NEWlem  34219  qqhval2  34279  esumfsup  34367  esumcvg  34383  cntnevol  34525  ddemeas  34533  dya2icoseg2  34575  dya2iocnei  34579  eulerpartlems  34657  eulerpartlemgvv  34673  eulerpart  34679  cndprobprob  34735  ballotlemsdom  34809  ballotth  34835  bnj945  35069  bnj1379  35125  bnj1459  35138  bnj557  35196  bnj571  35201  bnj849  35220  bnj964  35238  bnj978  35244  bnj1018g  35258  bnj1018  35259  bnj1020  35260  bnj1033  35264  bnj1175  35299  bnj1398  35329  bnj1417  35336  bnj1523  35366  nummin  35389  r1omhf  35402  axprALT2  35405  fineqvnttrclselem1  35417  onvf1odlem4  35449  onvf1od  35450  vonf1osev  35455  vonf1oonfo  35458  cusgr3cyclex  35486  txpconn  35582  satfv1  35713  satffun  35759  msubco  35881  mclsax  35919  dfon2lem7  36137  dfon2lem8  36138  pprodss4v  36232  fullfunfv  36297  altxpsspw  36327  funtransport  36381  fvtransport  36382  funray  36490  fvray  36491  funline  36492  fvline  36494  finminlem  36678  bisym1  36779  onsucconni  36797  onsucsuccmpi  36803  weiunse  36828  bj-currypara  37002  bj-cbvaw  37113  axc11n11r  37158  bj-equsal2  37310  bj-xpima1snALT  37442  bj-unexg  37523  bj-bm1.3ii  37549  bj-axseprep  37559  bj-axreprepsep  37560  bj-opelidb1ALT  37658  mptsnunlem  37832  iooelexlt  37856  relowlpssretop  37858  rdgeqoa  37864  difunieq  37868  nlpineqsn  37902  fvineqsneq  37906  wl-ax12v2cl  38000  wl-lem-nexmo  38070  matunitlindflem1  38115  ptrecube  38119  poimirlem26  38145  poimirlem30  38149  poimir  38152  ismblfin  38160  itg2addnclem  38170  dvasin  38203  sdclem2  38241  totbndbnd  38288  ismgmOLD  38349  exidresid  38378  isrngo  38396  rngoablo2  38408  rngoueqz  38439  isdivrngo  38449  isdrngo1  38455  isdrngo2  38457  ispridl2  38537  relcnveq3  38826  elrelscnveq3  39126  disjimeceqim  39303  dmqsblocks  39466  ax12eq  39565  ax12el  39566  lkr0f  39718  hl2at  40029  dalemswapyz  40280  pclfinclN  40574  osumcllem11N  40590  pexmidlem8N  40601  ltrnnid  40760  aks4d1p8  42704  redvmptabs  42969  sn-00id  43010  rictr  43138  eu6w  43258  mptfcl  43301  fphpd  43393  elmnc  43713  itgoval  43738  arearect  43792  reabsifpos  44210  clsk3nimkb  44616  grumnud  44862  nanorxor  44881  pm11.71  44973  iotavalsb  45009  sbiota1  45010  2uasbanh  45137  eel0TT  45279  eelT00  45280  eelTTT  45281  eelT11  45282  eelT12  45284  eelTT1  45285  eelT01  45286  eel0T1  45287  eelTT  45346  uunT1p1  45356  uun121  45358  uun121p1  45359  un2122  45365  uunTT1  45368  uunTT1p1  45369  uunTT1p2  45370  uunT11  45371  uunT11p1  45372  uunT11p2  45373  uunT12  45374  uunT12p1  45375  uunT12p2  45376  uunT12p3  45377  uunT12p4  45378  uunT12p5  45379  uun111  45380  3anidm12p2  45382  uun123  45383  3impdirp1  45391  undif3VD  45457  ax6e2ndeqVD  45484  2uasbanhVD  45486  ax6e2ndeqALT  45506  iunconnlem2  45510  sineq0ALT  45512  modelaxreplem1  45554  permaxrep  45582  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  stoweidlem3  46577  stoweidlem17  46591  fourierdlem42  46723  fourierdlem48  46728  fourierdlem50  46730  fourierdlem51  46731  fourierdlem76  46756  fourierdlem83  46763  fourierdlem87  46767  hoidmvval0  47161  evenwodadd  47463  rexrsb  47694  2reu8i  47707  2reuimp  47709  afv0nbfvbi  47745  afvfv0bi  47746  afveu  47747  fnbrafvb  47748  afvres  47766  tz6.12-afv  47767  dmfcoafv  47769  afvco2  47770  aovprc  47782  aovrcl  47783  aovmpt4g  47795  afv2eu  47832  afv2res  47833  tz6.12-afv2  47834  tz6.12i-afv2  47837  afv2rnfveq  47856  fvmptrab  47886  fvmptrabdm  47887  fzopred  47917  2ffzoeq  47922  muldvdsfacm1  47981  elsprel  48081  prproropf1o  48113  reupr  48128  lighneal  48220  odd2prm2  48340  even3prm2  48341  grictr  48545  grlimgrtrilem2  48624  usgrexmpl12ngric  48660  gpgprismgr4cycllem8  48724  gpgprismgr4cycllem11  48727  pgnbgreunbgrlem2lem1  48736  upgrwlkupwlk  48762  ovn0ssdmfun  48781  islinindfis  49071  rrx2linest  49364  line2ylem  49373  mofeu  49469  homf0  49630  uobffth  49839  uobeqw  49840  initopropd  49864  termopropd  49865  zeroopropd  49866  fucofvalne  49946  isthincd2  50058  lanrcl  50242  ranrcl  50243  setrec2fun  50313  elsetrecslem  50320  setrecsres  50323  secval  50368  cscval  50369  cotval  50370