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  1451  an42ds  1519  nanass  1539  19.38  1871  19.35  1909  19.8aw  2084  sbrimvw  2127  equsexv  2302  sbi2  2335  nfeqf2  2406  equsex  2447  dfmoeu  2560  2mo  2673  axie2  2727  necon1bi  2983  necon1i  2988  r19.35  3120  spc2ed  3555  reu6  3683  rabssrabd  4007  uneqin  4233  difin0ss  4320  inelcm  4417  falseral0OLD  4470  raaan2  4477  difprsn1  4759  tppreqb  4764  n0snor2el  4787  unissint  4931  intminss  4933  dfiun2g  4987  iununi  5058  triin  5228  eusv2nf  5357  reusv3i  5366  axprglem  5394  axprg  5395  moabexOLD  5427  opelopabt  5506  eqrelrel  5774  opeliunxp2  5816  opelrn  5926  ssxpb  6168  xpima  6176  xpimasn  6179  dmsn0el  6215  relcnvtrOLD  6273  relcoi2  6283  elsnxp  6297  reuop  6299  iotanul  6522  dffv2  6985  fnfvrnss  7126  fressnfv  7169  fconst5  7216  f1mpt  7269  isocnv3  7344  f1owe  7365  f1oweOLD  7366  ovprc  7462  fvmpopr2d  7586  ovn0ssdmfun  7593  onminesb  7811  onminsb  7812  onintrab  7814  onnminsb  7817  ordsuci  7826  onsucuni2  7849  tfindsg2  7877  zfrep6OLD  7971  fo1stres  8031  fo2ndres  8032  bropopvvv  8106  bropfvvvv  8108  frxp  8145  poseq  8182  soseq  8183  opeliunxp2f  8235  mpoxopoveqd  8246  reldmtpos  8259  frrlem4  8315  tfrlem5  8395  tfrlem9  8401  tfr2  8414  rdgsuc  8440  oaordi  8562  oeordi  8604  omopthi  8678  on2recsov  8685  fvmptmap  8917  mptelixpg  8971  ener  9036  domtr  9042  unen  9081  undom  9092  dom0  9132  xpf1o  9166  mapen  9168  pssnn  9192  unfi  9194  ssfi  9196  ensymfib  9207  entrfil  9208  enfii  9209  domtrfil  9215  unxpdomlem3  9257  isinf  9264  frfi  9284  unblem1  9292  fofinf1o  9329  fsuppun  9386  elirrvOLD  9599  inf3lem2  9637  inf3lem5  9640  cantnfp1lem1  9686  cantnfp1lem3  9688  tcmin  9747  setinds  9757  frr2  9771  r1ordg  9792  r1ord  9794  rankr1ai  9813  r1val3  9857  bndrank  9861  unbndrank  9862  rankr1b  9888  rankxplim3  9905  tcrank  9908  setrec2fun  9980  xpnum  10039  cardmin2  10087  infxpenlem  10099  fseqen  10113  dfac8clem  10118  alephsson  10186  alephfp  10194  dfac4  10208  kmlem6  10241  kmlem8  10243  kmlem9  10244  cflem  10330  infpssr  10393  fin1a2lem12  10496  axcc4  10524  axcc4dom  10526  ac6s2  10571  zornn0g  10590  cardidg  10639  unsnen  10644  pwcfsdom  10675  cfpwsdom  10676  gchpwdom  10762  r1tskina  10874  intgru  10906  indpi  10999  nqereu  11021  supsrlem  11203  letrii  11442  dfnn3  12356  zaddcl  12743  nn0ind  12801  fnn0ind  12805  ublbneg  13067  nn01to3  13075  infmrp1  13482  fz0  13679  fzo1fzo0n0  13857  elfzom1elp1fzo  13874  fzo0end  13900  elfznelfzo  13915  fzind2  13930  injresinjlem  13932  fleqceilz  14001  nnsinds  14138  nn0sinds  14139  faclbnd4lem1  14444  hashinf  14486  hasheqf1oi  14502  hashgt0elex  14552  hashgt23el  14576  hashfacen  14606  hash2prde  14622  hash2sspr  14641  fun2dmnop0  14656  iswrddm0  14690  swrdnnn0nd  14814  swrdnd0  14815  swrdlsw  14825  pfxn0  14844  pfxnd0  14846  swrdswrdlem  14861  pfxccatin12lem3  14889  pfxccat3  14891  pfxccat3a  14895  swrdccat3blem  14896  cshwsublen  14955  cshwidxmod  14962  repswcshw  14971  cshw1  14981  trclun  15176  dmtrclfv  15180  sgn3da  15263  rediv  15307  imdiv  15314  fsump1i  15944  modfsummods  15969  bpolydiflem  16229  bpoly3  16233  bpoly4  16234  cos1bnd  16364  sinltx  16366  rpnnen2lem1  16391  rpnnen2lem2  16392  rpnnen2lem12  16402  odd2np1  16520  opoe  16542  omoe  16543  opeo  16544  omeo  16545  gcdcllem1  16678  gcdaddmlem  16705  dfgcd2  16728  algfx  16764  lcmledvds  16783  lcmfunsnlem  16825  lcmfun  16829  coprmprod  16845  coprmproddvdslem  16846  odzval  16978  odzdvds  16982  prmreclem5  17107  mul4sq  17141  prmgaplem5  17242  prmgaplem6  17243  imasaddfnlem  17709  mreexexlem4d  17830  joindmss  18560  meetdmss  18574  gictr  19499  cntzval  19544  symg2bas  19616  odfval  19755  efgsfo  19962  efgrelexlemb  19973  dprddomcld  20226  dprdsubg  20249  dprd2da  20267  rictr  20761  isdrng3lem1  21014  isdrng3  21016  lssacs  21251  prmidl2  21631  cnfldinv  21718  pzriprnglem7  21802  ocvval  21982  selvval  22438  dmatmul  22821  mdetfval1  22914  mndifsplit  22960  matunitlindflem1  23003  fvmptnn04if  23176  toprntopon  23252  opnnei  23447  ordtbas2  23518  ordtrest2lem  23530  lmmo  23707  fincmp  23720  bwth  23737  txbas  23895  ptcnplem  23949  tx2ndc  23979  hmphtr  24111  fbun  24168  filconn  24211  ptcmplem5  24384  cnextcn  24395  utoptop  24562  ucncn  24612  metust  24886  cfilucfil  24887  elcncf1di  25225  xrhmeo  25276  phtpycc  25321  copco  25348  pcohtpylem  25349  pcopt  25352  pcopt2  25353  ncvsi  25481  ovolval  25803  iunmbl2  25887  itg2splitlem  26078  cpnfval  26261  plyval  26520  fta1  26638  aaliou2b  26677  tayl0  26698  ulmdvlem3  26738  radcnvlem2  26750  dvradcnv  26757  reeff1o  26783  sincosq1lem  26835  sincosq2sgn  26837  sincosq4sgn  26839  sinq12ge0  26846  logrncl  26904  eflog  26913  cxpge0  27020  logb1  27106  atanf  27217  atanbnd  27263  igamf  27387  igamcl  27388  lgsne0  27671  mul2sq  27755  2sqreultblem  27784  pntibnd  27929  ostth  27975  nobdaymin  28148  nocvxminlem  28149  cutlt  28327  norec2ov  28352  addsuniflem  28396  mulsuniflem  28544  oldfib  28772  zmulscld  28792  zseo  28817  z12addscl  28872  mpteleeOLD  29482  axlowdimlem9  29537  axlowdimlem12  29540  axcontlem2  29552  axcontlem12  29562  structgrssvtx  29611  structgrssiedg  29612  lpvtx  29655  nbuhgr  29933  nbumgr  29937  nbuhgr2vtx1edgblem  29941  nbgr0edglem  29946  nbgr1vtx  29948  uvtx01vtx  29987  prcliscplgr  30004  cusgrsizeinds  30042  sizusglecusglem2  30052  uhgrvd00  30124  fusgrregdegfi  30159  rusgr1vtxlem  30177  wlkeq  30223  wlk1walk  30228  uspgr2wlkeq  30235  wlklenvclwlk  30243  wlkreslem  30257  wlkdlem2  30271  wlkdlem4  30273  spthonepeq  30347  cyclnumvtx  30397  clwlkclwwlkflem  30604  clwlkclwwlkfolem  30607  clwlkclwwlkf  30608  clwwisshclwws  30615  clwwlkneq0  30629  3wlkdlem6  30775  eupth2eucrct  30827  eupth2lem1  30828  eupth2lem3lem7  30844  frgr3vlem1  30883  frgr3vlem2  30884  frgrncvvdeqlem8  30916  frgrncvvdeqlem9  30917  numclwwlk5  30998  frgrreg  31004  frgrregord013  31005  friendshipgt3  31008  isgrpo  31108  vciOLD  31172  vcex  31189  nmogtmnf  31381  siilem1  31462  siii  31464  ajmoi  31469  bcsiALT  31790  hhcms  31814  ocval  31891  hsupval  31945  omlsilem  32013  h1de2bi  32165  h1de2ctlem  32166  hosubeq0i  32437  adjmo  32443  nmopgtmnf  32479  nlfnval  32492  nmcopex  32640  nmcfnex  32664  riesz4i  32674  riesz1  32676  riesz2  32677  opsqrlem1  32751  superpos  32965  hatomistici  32973  chpssati  32974  mdsymlem3  33016  3o1cs  33110  3o2cs  33111  3o3cs  33112  iunrnmptss  33210  brabgaf  33251  f1mptrn  33280  ffsrn  33370  xnn0gt0  33411  hashxpe  33449  elrgspnlem4  33856  mxidlnzrb  34054  evl1deg2  34159  evl1deg3  34160  fedgmul  34313  cos9thpiminplylem2  34465  ordtrest2NEWlem  34604  qqhval2  34664  esumfsup  34752  esumcvg  34768  cntnevol  34911  ddemeas  34919  dya2icoseg2  34960  dya2iocnei  34964  eulerpartlems  35042  eulerpartlemgvv  35058  eulerpart  35064  cndprobprob  35120  ballotlemsdom  35194  ballotth  35220  bnj945  35454  bnj1379  35510  bnj1459  35523  bnj557  35581  bnj571  35586  bnj849  35605  bnj964  35623  bnj978  35629  bnj1018g  35643  bnj1018  35644  bnj1020  35645  bnj1033  35649  bnj1175  35684  bnj1398  35714  bnj1417  35721  bnj1523  35751  reu6f  35759  nummin  35780  r1omfi  35788  axprALT2  35792  werankwe  35797  dfac16  35822  fineqvnttrclselem1  35857  rankkardu  35907  maxssj0  35957  j0ltaleph  35959  onvf1odlem4  35985  onvf1od  35986  vonf1osev  35991  onprcf1acwevdlem2  35997  vonf1oonfo  36000  cusgr3cyclex  36019  txpconn  36115  satfv1  36246  satffun  36292  msubco  36414  mclsax  36452  dfon2lem7  36675  dfon2lem8  36676  pprodss4v  36770  fullfunfv  36835  altxpsspw  36866  funtransport  36920  fvtransport  36921  funray  37029  fvray  37030  funline  37031  fvline  37033  finminlem  37230  bisym1  37331  onsucconni  37349  onsucsuccmpi  37355  weiunse  37380  bj-currypara  37553  bj-cbvaw  37664  axc11n11r  37709  bj-equsal2  37861  bj-xpima1snALT  37994  bj-unexg  38075  bj-bm1.3ii  38115  bj-axseprep  38126  bj-axreprepsep  38127  bj-opelidb1ALT  38224  mptsnunlem  38398  iooelexlt  38422  relowlpssretop  38424  rdgeqoa  38430  difunieq  38434  nlpineqsn  38468  fvineqsneq  38472  wl-ax12v2cl  38566  wl-lem-nexmo  38636  ptrecube  38675  poimirlem26  38701  poimirlem30  38705  poimir  38708  ismblfin  38716  itg2addnclem  38726  dvasin  38759  sdclem2  38813  totbndbnd  38860  ismgmOLD  38921  exidresid  38950  isrngo  38968  rngoablo2  38980  rngoueqz  39011  isdivrngo  39021  isdrngo1  39027  isdrngo2  39029  ispridl2  39109  relcnveq3  39396  elrelscnveq3  39696  disjimeceqim  39873  dmqsblocks  40036  ax12eq  40135  ax12el  40136  lkr0f  40288  hl2at  40599  dalemswapyz  40850  pclfinclN  41144  osumcllem11N  41160  pexmidlem8N  41171  ltrnnid  41330  aks4d1p8  43274  redvmptabs  43548  sn-00id  43589  eu6w  43824  mptfcl  43868  fphpd  43960  elmnc  44275  itgoval  44300  arearect  44354  reabsifpos  44771  clsk3nimkb  45177  grumnud  45407  nanorxor  45426  pm11.71  45518  iotavalsb  45553  sbiota1  45554  2uasbanh  45680  eel0TT  45822  eelT00  45823  eelTTT  45824  eelT11  45825  eelT12  45827  eelTT1  45828  eelT01  45829  eel0T1  45830  eelTT  45889  uunT1p1  45899  uun121  45901  uun121p1  45902  un2122  45908  uunTT1  45911  uunTT1p1  45912  uunTT1p2  45913  uunT11  45914  uunT11p1  45915  uunT11p2  45916  uunT12  45917  uunT12p1  45918  uunT12p2  45919  uunT12p3  45920  uunT12p4  45921  uunT12p5  45922  uun111  45923  3anidm12p2  45925  uun123  45926  3impdirp1  45934  undif3VD  46000  ax6e2ndeqVD  46027  2uasbanhVD  46029  ax6e2ndeqALT  46049  iunconnlem2  46053  sineq0ALT  46055  modelaxreplem1  46104  permaxrep  46132  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  stoweidlem3  47149  stoweidlem17  47163  fourierdlem42  47295  fourierdlem48  47300  fourierdlem50  47302  fourierdlem51  47303  fourierdlem76  47328  fourierdlem83  47335  fourierdlem87  47339  hoidmvval0  47733  evenwodadd  48047  rexrsb  48307  2reu8i  48320  2reuimp  48322  afv0nbfvbi  48357  afvfv0bi  48358  afveu  48359  fnbrafvb  48360  afvres  48378  tz6.12-afv  48379  dmfcoafv  48381  afvco2  48382  aovprc  48394  aovrcl  48395  aovmpt4g  48407  afv2eu  48444  afv2res  48445  tz6.12-afv2  48446  tz6.12i-afv2  48449  afv2rnfveq  48468  fvmptrab  48498  fvmptrabdm  48499  fzopred  48529  2ffzoeq  48534  muldvdsfacm1  48593  elsprel  48693  prproropf1o  48725  reupr  48740  lighneal  48832  odd2prm2  48952  even3prm2  48953  grictr  49157  grlimgrtrilem2  49236  usgrexmpl12ngric  49272  gpgprismgr4cycllem8  49336  gpgprismgr4cycllem11  49339  pgnbgreunbgrlem2lem1  49348  upgrwlkupwlk  49374  islinindfis  49697  rrx2linest  49990  line2ylem  49999  mofeu  50095  homf0  50259  uobffth  50470  uobeqw  50471  initopropd  50501  termopropd  50502  zeroopropd  50503  fucofvalne  50583  isthincd2  50708  lanrcl  50940  ranrcl  50941  elsetrecslem  51003  setrecsres  51006  secval  51051  cscval  51052  cotval  51053