Theorem sylbir 238

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3i  294  ex  418  3expa  1136  3ori  1452  an42ds  1520  nanass  1540  19.38  1872  19.35  1912  19.8aw  2087  sbrimvw  2130  equsexv  2306  sbi2  2339  nfeqf2  2409  equsex  2450  dfmoeu  2563  2mo  2676  axie2  2730  necon1bi  2987  necon1i  2992  r19.35  3124  spc2ed  3559  reu6  3687  rabssrabd  4011  uneqin  4237  difin0ss  4324  inelcm  4421  falseral0OLD  4474  raaan2  4481  difprsn1  4765  tppreqb  4770  n0snor2el  4793  unissint  4937  intminss  4939  dfiun2g  4993  iununi  5064  triin  5235  eusv2nf  5364  reusv3i  5373  axprglem  5401  axprg  5402  moabexOLD  5434  opelopabt  5513  eqrelrel  5782  opeliunxp2  5825  opelrn  5937  ssxpb  6184  xpima  6192  xpimasn  6195  dmsn0el  6231  relcnvtrOLD  6294  relcoi2  6304  elsnxp  6320  reuop  6322  iotanul  6545  dffv2  7011  fnfvrnss  7153  fressnfv  7196  fconst5  7243  f1mpt  7296  isocnv3  7371  f1owe  7392  f1oweOLD  7393  ovprc  7489  fvmpopr2d  7614  ovn0ssdmfun  7621  onminesb  7841  onminsb  7842  onintrab  7844  onnminsb  7847  ordsuci  7856  onsucuni2  7879  tfindsg2  7907  zfrep6OLD  8001  fo1stres  8061  fo2ndres  8062  bropopvvv  8136  bropfvvvv  8138  frxp  8175  poseq  8212  soseq  8213  opeliunxp2f  8265  mpoxopoveqd  8276  reldmtpos  8289  frrlem4  8345  tfrlem5  8425  tfrlem9  8431  tfr2  8444  rdgsuc  8470  oaordi  8592  oeordi  8634  omopthi  8708  on2recsov  8715  fvmptmap  8947  mptelixpg  9001  ener  9066  domtr  9072  unen  9111  undom  9122  dom0  9162  xpf1o  9196  mapen  9198  pssnn  9222  unfi  9224  ssfi  9226  ensymfib  9237  entrfil  9238  enfii  9239  domtrfil  9245  unxpdomlem3  9287  isinf  9294  frfi  9314  unblem1  9322  fofinf1o  9359  fsuppun  9416  elirrvOLD  9629  inf3lem2  9667  inf3lem5  9670  cantnfp1lem1  9716  cantnfp1lem3  9718  tcmin  9777  setinds  9787  frr2  9801  r1ordg  9822  r1ord  9824  rankr1ai  9843  r1val3  9887  bndrank  9891  unbndrank  9892  rankr1b  9918  rankxplim3  9935  tcrank  9938  setrec2fun  10010  xpnum  10069  cardmin2  10119  infxpenlem  10131  fseqen  10145  dfac8clem  10150  alephsson  10218  alephfp  10226  dfac4  10240  kmlem6  10273  kmlem8  10275  kmlem9  10276  cflem  10362  infpssr  10425  fin1a2lem12  10528  axcc4  10556  axcc4dom  10558  ac6s2  10603  zornn0g  10622  cardidg  10671  unsnen  10676  pwcfsdom  10707  cfpwsdom  10708  gchpwdom  10794  r1tskina  10906  intgru  10938  indpi  11031  nqereu  11053  supsrlem  11235  letrii  11474  dfnn3  12389  zaddcl  12776  nn0ind  12834  fnn0ind  12838  ublbneg  13100  nn01to3  13108  infmrp1  13515  fz0  13712  fzo1fzo0n0  13890  elfzom1elp1fzo  13907  fzo0end  13933  elfznelfzo  13948  fzind2  13963  injresinjlem  13965  fleqceilz  14034  nnsinds  14171  nn0sinds  14172  faclbnd4lem1  14478  hashinf  14520  hasheqf1oi  14536  hashgt0elex  14586  hashgt23el  14610  hashfacen  14640  hash2prde  14656  hash2sspr  14675  fun2dmnop0  14690  iswrddm0  14724  swrdnnn0nd  14848  swrdnd0  14849  swrdlsw  14859  pfxn0  14878  pfxnd0  14880  swrdswrdlem  14895  pfxccatin12lem3  14923  pfxccat3  14925  pfxccat3a  14929  swrdccat3blem  14930  cshwsublen  14989  cshwidxmod  14996  repswcshw  15005  cshw1  15015  trclun  15210  dmtrclfv  15214  sgn3da  15297  rediv  15341  imdiv  15348  fsump1i  15979  modfsummods  16004  bpolydiflem  16264  bpoly3  16268  bpoly4  16269  cos1bnd  16399  sinltx  16401  rpnnen2lem1  16426  rpnnen2lem2  16427  rpnnen2lem12  16437  odd2np1  16555  opoe  16577  omoe  16578  opeo  16579  omeo  16580  gcdcllem1  16713  gcdaddmlem  16740  dfgcd2  16763  algfx  16799  lcmledvds  16818  lcmfunsnlem  16860  lcmfun  16864  coprmprod  16880  coprmproddvdslem  16881  odzval  17013  odzdvds  17017  prmreclem5  17142  mul4sq  17176  prmgaplem5  17277  prmgaplem6  17278  imasaddfnlem  17750  mreexexlem4d  17871  joindmss  18601  meetdmss  18615  gictr  19541  cntzval  19586  symg2bas  19658  odfval  19797  efgsfo  20004  efgrelexlemb  20015  dprddomcld  20268  dprdsubg  20291  dprd2da  20309  rictr  20803  isdrng3lem1  21056  isdrng3  21058  lssacs  21293  prmidl2  21673  cnfldinv  21761  pzriprnglem7  21848  ocvval  22028  selvval  22484  dmatmul  22867  mdetfval1  22960  mndifsplit  23006  matunitlindflem1  23049  fvmptnn04if  23222  toprntopon  23298  opnnei  23493  ordtbas2  23564  ordtrest2lem  23576  lmmo  23753  fincmp  23766  bwth  23783  txbas  23941  ptcnplem  23995  tx2ndc  24025  hmphtr  24157  fbun  24214  filconn  24257  ptcmplem5  24430  cnextcn  24441  utoptop  24608  ucncn  24658  metust  24932  cfilucfil  24933  elcncf1di  25271  xrhmeo  25322  phtpycc  25367  copco  25394  pcohtpylem  25395  pcopt  25398  pcopt2  25399  ncvsi  25527  ovolval  25849  iunmbl2  25933  itg2splitlem  26124  cpnfval  26307  plyval  26566  fta1  26684  aaliou2b  26725  tayl0  26746  ulmdvlem3  26786  radcnvlem2  26798  dvradcnv  26805  reeff1o  26831  sincosq1lem  26883  sincosq2sgn  26885  sincosq4sgn  26887  sinq12ge0  26894  logrncl  26952  eflog  26961  cxpge0  27068  logb1  27154  atanf  27265  atanbnd  27311  igamf  27435  igamcl  27436  lgsne0  27719  mul2sq  27803  2sqreultblem  27832  pntibnd  27977  ostth  28023  nobdaymin  28196  nocvxminlem  28197  cutlt  28375  norec2ov  28400  addsuniflem  28444  mulsuniflem  28592  oldfib  28820  zmulscld  28840  zseo  28865  z12addscl  28920  mpteleeOLD  29530  axlowdimlem9  29585  axlowdimlem12  29588  axcontlem2  29600  axcontlem12  29610  structgrssvtx  29659  structgrssiedg  29660  lpvtx  29703  nbuhgr  29981  nbumgr  29985  nbuhgr2vtx1edgblem  29989  nbgr0edglem  29994  nbgr1vtx  29996  uvtx01vtx  30035  prcliscplgr  30052  cusgrsizeinds  30090  sizusglecusglem2  30100  uhgrvd00  30172  fusgrregdegfi  30207  rusgr1vtxlem  30225  wlkeq  30271  wlk1walk  30276  uspgr2wlkeq  30283  wlklenvclwlk  30291  wlkreslem  30305  wlkdlem2  30319  wlkdlem4  30321  spthonepeq  30395  cyclnumvtx  30445  clwlkclwwlkflem  30652  clwlkclwwlkfolem  30655  clwlkclwwlkf  30656  clwwisshclwws  30663  clwwlkneq0  30677  3wlkdlem6  30823  eupth2eucrct  30875  eupth2lem1  30876  eupth2lem3lem7  30892  frgr3vlem1  30931  frgr3vlem2  30932  frgrncvvdeqlem8  30964  frgrncvvdeqlem9  30965  numclwwlk5  31046  frgrreg  31052  frgrregord013  31053  friendshipgt3  31056  isgrpo  31156  vciOLD  31220  vcex  31237  nmogtmnf  31429  siilem1  31510  siii  31512  ajmoi  31517  bcsiALT  31838  hhcms  31862  ocval  31939  hsupval  31993  omlsilem  32061  h1de2bi  32213  h1de2ctlem  32214  hosubeq0i  32485  adjmo  32491  nmopgtmnf  32527  nlfnval  32540  nmcopex  32688  nmcfnex  32712  riesz4i  32722  riesz1  32724  riesz2  32725  opsqrlem1  32799  superpos  33013  hatomistici  33021  chpssati  33022  mdsymlem3  33064  3o1cs  33158  3o2cs  33159  3o3cs  33160  iunrnmptss  33257  brabgaf  33298  f1mptrn  33327  ffsrn  33416  xnn0gt0  33457  hashxpe  33495  elrgspnlem4  33905  mxidlnzrb  34108  evl1deg2  34212  evl1deg3  34213  fedgmul  34374  cos9thpiminplylem2  34526  ordtrest2NEWlem  34665  qqhval2  34725  esumfsup  34813  esumcvg  34829  cntnevol  34972  ddemeas  34980  dya2icoseg2  35021  dya2iocnei  35025  eulerpartlems  35103  eulerpartlemgvv  35119  eulerpart  35125  cndprobprob  35181  ballotlemsdom  35255  ballotth  35281  bnj945  35515  bnj1379  35571  bnj1459  35584  bnj557  35642  bnj571  35647  bnj849  35666  bnj964  35684  bnj978  35690  bnj1018g  35704  bnj1018  35705  bnj1020  35706  bnj1033  35710  bnj1175  35745  bnj1398  35775  bnj1417  35782  bnj1523  35812  reu6f  35820  nummin  35847  axprALT2  35857  werankwe  35862  dfac16  35887  fineqvnttrclselem1  35930  rankkardu  35980  maxssj0  36047  j0ltaleph  36049  onvf1odlem4  36075  onvf1od  36076  vonf1osev  36081  onprcf1acwevdlem2  36087  vonf1oonfo  36090  cusgr3cyclex  36109  txpconn  36205  satfv1  36336  satffun  36382  msubco  36504  mclsax  36542  mirimanofffr  36670  dfon2lem7  36766  dfon2lem8  36767  pprodss4v  36861  fullfunfv  36926  altxpsspw  36957  funtransport  37011  fvtransport  37012  funray  37120  fvray  37121  funline  37122  fvline  37124  finminlem  37321  bisym1  37422  onsucconni  37440  onsucsuccmpi  37446  weiunse  37471  bj-currypara  37644  bj-cbvaw  37755  axc11n11r  37800  bj-equsal2  37952  bj-xpima1snALT  38085  bj-unexg  38166  bj-opelresdm  38182  bj-bm1.3ii  38249  bj-axseprep  38260  bj-axreprepsep  38261  bj-opelidb1ALT  38355  mptsnunlem  38529  iooelexlt  38553  relowlpssretop  38555  rdgeqoa  38561  difunieq  38565  nlpineqsn  38599  fvineqsneq  38603  wl-ax12v2cl  38697  wl-lem-nexmo  38767  ptrecube  38806  poimirlem26  38832  poimirlem30  38836  poimir  38839  ismblfin  38847  itg2addnclem  38857  dvasin  38890  sdclem2  38942  totbndbnd  38989  ismgmOLD  39050  exidresid  39079  isrngo  39097  rngoablo2  39109  rngoueqz  39140  isdivrngo  39150  isdrngo1  39156  isdrngo2  39158  ispridl2  39238  relcnveq3  39525  elrelscnveq3  39825  disjimeceqim  40002  dmqsblocks  40165  ax12eq  40264  ax12el  40265  lkr0f  40417  hl2at  40728  dalemswapyz  40979  pclfinclN  41273  osumcllem11N  41289  pexmidlem8N  41300  ltrnnid  41459  aks4d1p8  43403  redvmptabs  43677  sn-00id  43718  eu6w  43953  mptfcl  43997  fphpd  44089  elmnc  44403  itgoval  44428  arearect  44478  reabsifpos  44895  clsk3nimkb  45301  grumnud  45531  nanorxor  45550  pm11.71  45642  iotavalsb  45677  sbiota1  45678  2uasbanh  45804  eel0TT  45946  eelT00  45947  eelTTT  45948  eelT11  45949  eelT12  45951  eelTT1  45952  eelT01  45953  eel0T1  45954  eelTT  46013  uunT1p1  46023  uun121  46025  uun121p1  46026  un2122  46032  uunTT1  46035  uunTT1p1  46036  uunTT1p2  46037  uunT11  46038  uunT11p1  46039  uunT11p2  46040  uunT12  46041  uunT12p1  46042  uunT12p2  46043  uunT12p3  46044  uunT12p4  46045  uunT12p5  46046  uun111  46047  3anidm12p2  46049  uun123  46050  3impdirp1  46058  undif3VD  46124  ax6e2ndeqVD  46151  2uasbanhVD  46153  ax6e2ndeqALT  46173  iunconnlem2  46177  sineq0ALT  46179  modelaxreplem1  46232  permaxrep  46260  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweidlem3  47286  stoweidlem17  47300  fourierdlem42  47432  fourierdlem48  47437  fourierdlem50  47439  fourierdlem51  47440  fourierdlem76  47465  fourierdlem83  47472  fourierdlem87  47476  hoidmvval0  47870  evenwodadd  48184  rexrsb  48444  2reu8i  48457  2reuimp  48459  afv0nbfvbi  48494  afvfv0bi  48495  afveu  48496  fnbrafvb  48497  afvres  48515  tz6.12-afv  48516  dmfcoafv  48518  afvco2  48519  aovprc  48531  aovrcl  48532  aovmpt4g  48544  afv2eu  48581  afv2res  48582  tz6.12-afv2  48583  tz6.12i-afv2  48586  afv2rnfveq  48605  fvmptrab  48635  fvmptrabdm  48636  fzopred  48666  2ffzoeq  48671  muldvdsfacm1  48730  elsprel  48830  prproropf1o  48862  reupr  48877  lighneal  48969  odd2prm2  49089  even3prm2  49090  grictr  49294  grlimgrtrilem2  49373  usgrexmpl12ngric  49409  gpgprismgr4cycllem8  49473  gpgprismgr4cycllem11  49476  pgnbgreunbgrlem2lem1  49485  upgrwlkupwlk  49511  islinindfis  49892  rrx2linest  50185  line2ylem  50194  mofeu  50290  homf0  50454  uobffth  50665  uobeqw  50666  initopropd  50696  termopropd  50697  zeroopropd  50698  fucofvalne  50778  isthincd2  50903  lanrcl  51135  ranrcl  51136  elsetrecslem  51198  setrecsres  51201  tanhcl  51250  secval  51268  cscval  51269  cotval  51270