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  1520  nanass  1540  19.38  1872  19.35  1910  19.8aw  2085  sbrimvw  2128  equsexv  2302  sbi2  2335  nfeqf2  2406  equsex  2447  dfmoeu  2560  2mo  2673  axie2  2727  necon1bi  2983  necon1i  2988  r19.35  3120  spc2ed  3555  reu6  3684  rabssrabd  4031  uneqin  4235  difin0ss  4321  inelcm  4418  falseral0OLD  4471  raaan2  4478  difprsn1  4763  tppreqb  4768  n0snor2el  4793  unissint  4932  intminss  4934  dfiun2g  4988  iununi  5059  triin  5229  bm1.3iiOLD  5259  eusv2nf  5360  reusv3i  5369  axprglem  5401  axprg  5402  moabexOLD  5434  opelopabt  5510  eqrelrel  5777  opeliunxp2  5818  opelrn  5927  ssxpb  6167  xpima  6175  xpimasn  6178  dmsn0el  6207  relcnvtrOLD  6265  relcoi2  6275  elsnxp  6289  reuop  6291  iotanul  6513  dffv2  6974  fnfvrnss  7115  fressnfv  7158  fconst5  7206  f1mpt  7259  isocnv3  7334  f1owe  7355  f1oweOLD  7356  ovprc  7452  fvmpopr2d  7576  ovn0ssdmfun  7583  onminesb  7793  onminsb  7794  onintrab  7796  onnminsb  7799  ordsuci  7808  onsucuni2  7831  tfindsg2  7859  zfrep6OLD  7953  fo1stres  8013  fo2ndres  8014  bropopvvv  8088  bropfvvvv  8090  frxp  8125  poseq  8157  soseq  8158  opeliunxp2f  8209  mpoxopoveqd  8220  reldmtpos  8233  frrlem4  8289  tfrlem5  8369  tfrlem9  8375  tfr2  8388  rdgsuc  8414  oaordi  8534  oeordi  8576  omopthi  8650  on2recsov  8657  fvmptmap  8889  mptelixpg  8943  ener  9008  domtr  9014  unen  9053  undom  9064  dom0  9104  xpf1o  9138  mapen  9140  pssnn  9164  unfi  9166  ssfi  9168  ensymfib  9179  entrfil  9180  enfii  9181  domtrfil  9187  unxpdomlem3  9229  isinf  9236  frfi  9256  unblem1  9263  fofinf1o  9300  fsuppun  9358  elirrvOLD  9571  inf3lem2  9609  inf3lem5  9612  cantnfp1lem1  9658  cantnfp1lem3  9660  tcmin  9719  setinds  9729  frr2  9743  r1ordg  9761  r1ord  9763  rankr1ai  9781  r1val3  9821  bndrank  9824  unbndrank  9825  rankr1b  9847  rankxplim3  9864  tcrank  9867  xpnum  9957  cardmin2  10005  infxpenlem  10017  fseqen  10031  dfac8clem  10036  alephsson  10104  alephfp  10112  dfac4  10126  kmlem6  10159  kmlem8  10161  kmlem9  10162  cflem  10248  infpssr  10311  fin1a2lem12  10414  axcc4  10442  axcc4dom  10444  ac6s2  10489  zornn0g  10508  cardidg  10557  unsnen  10562  pwcfsdom  10593  cfpwsdom  10594  gchpwdom  10680  r1tskina  10792  intgru  10824  indpi  10917  nqereu  10939  supsrlem  11121  letrii  11360  dfnn3  12272  zaddcl  12659  nn0ind  12717  fnn0ind  12721  ublbneg  12983  nn01to3  12991  infmrp1  13398  fz0  13594  fzo1fzo0n0  13772  elfzom1elp1fzo  13789  fzo0end  13815  elfznelfzo  13830  fzind2  13845  injresinjlem  13847  fleqceilz  13916  nnsinds  14053  nn0sinds  14054  faclbnd4lem1  14358  hashinf  14400  hasheqf1oi  14416  hashgt0elex  14466  hashgt23el  14490  hashfacen  14520  hash2prde  14536  hash2sspr  14555  fun2dmnop0  14570  iswrddm0  14604  swrdnnn0nd  14727  swrdnd0  14728  swrdlsw  14738  pfxn0  14757  pfxnd0  14759  swrdswrdlem  14774  pfxccatin12lem3  14802  pfxccat3  14804  pfxccat3a  14808  swrdccat3blem  14809  cshwsublen  14868  cshwidxmod  14875  repswcshw  14884  cshw1  14894  trclun  15088  dmtrclfv  15092  sgn3da  15175  rediv  15219  imdiv  15226  fsump1i  15856  modfsummods  15881  bpolydiflem  16141  bpoly3  16145  bpoly4  16146  cos1bnd  16276  sinltx  16278  rpnnen2lem1  16303  rpnnen2lem2  16304  rpnnen2lem12  16314  odd2np1  16432  opoe  16454  omoe  16455  opeo  16456  omeo  16457  gcdcllem1  16590  gcdaddmlem  16615  dfgcd2  16637  algfx  16671  lcmledvds  16690  lcmfunsnlem  16732  lcmfun  16736  coprmprod  16752  coprmproddvdslem  16753  odzval  16884  odzdvds  16888  prmreclem5  17013  mul4sq  17047  prmgaplem5  17148  prmgaplem6  17149  imasaddfnlem  17615  mreexexlem4d  17736  joindmss  18466  meetdmss  18480  gictr  19404  cntzval  19449  symg2bas  19521  odfval  19660  efgsfo  19867  efgrelexlemb  19878  dprddomcld  20131  dprdsubg  20154  dprd2da  20172  rictr  20664  isdrng3lem1  20915  isdrng3  20917  lssacs  21152  prmidl2  21530  cnfldinv  21617  pzriprnglem7  21701  ocvval  21881  selvval  22337  dmatmul  22720  mdetfval1  22813  mndifsplit  22859  matunitlindflem1  22902  fvmptnn04if  23075  toprntopon  23151  opnnei  23346  ordtbas2  23417  ordtrest2lem  23429  lmmo  23606  fincmp  23619  bwth  23636  txbas  23794  ptcnplem  23848  tx2ndc  23878  hmphtr  24010  fbun  24067  filconn  24110  ptcmplem5  24283  cnextcn  24294  utoptop  24461  ucncn  24511  metust  24785  cfilucfil  24786  elcncf1di  25124  xrhmeo  25175  phtpycc  25220  copco  25247  pcohtpylem  25248  pcopt  25251  pcopt2  25252  ncvsi  25380  ovolval  25702  iunmbl2  25786  itg2splitlem  25977  cpnfval  26160  plyval  26419  fta1  26539  aaliou2b  26578  tayl0  26599  ulmdvlem3  26639  radcnvlem2  26651  dvradcnv  26658  reeff1o  26684  sincosq1lem  26736  sincosq2sgn  26738  sincosq4sgn  26740  sinq12ge0  26747  logrncl  26805  eflog  26814  cxpge0  26921  logb1  27007  atanf  27118  atanbnd  27164  igamf  27288  igamcl  27289  lgsne0  27572  mul2sq  27656  2sqreultblem  27685  pntibnd  27830  ostth  27876  nobdaymin  28019  nocvxminlem  28020  cutlt  28198  norec2ov  28223  addsuniflem  28267  mulsuniflem  28415  oldfib  28643  zmulscld  28663  zseo  28688  z12addscl  28743  mpteleeOLD  29353  axlowdimlem9  29408  axlowdimlem12  29411  axcontlem2  29423  axcontlem12  29433  structgrssvtx  29482  structgrssiedg  29483  lpvtx  29526  nbuhgr  29804  nbumgr  29808  nbuhgr2vtx1edgblem  29812  nbgr0edglem  29817  nbgr1vtx  29819  uvtx01vtx  29858  prcliscplgr  29875  cusgrsizeinds  29913  sizusglecusglem2  29923  uhgrvd00  29995  fusgrregdegfi  30030  rusgr1vtxlem  30048  wlkeq  30094  wlk1walk  30099  uspgr2wlkeq  30106  wlklenvclwlk  30114  wlkreslem  30128  wlkdlem2  30142  wlkdlem4  30144  spthonepeq  30218  cyclnumvtx  30268  clwlkclwwlkflem  30475  clwlkclwwlkfolem  30478  clwlkclwwlkf  30479  clwwisshclwws  30486  clwwlkneq0  30500  3wlkdlem6  30646  eupth2eucrct  30698  eupth2lem1  30699  eupth2lem3lem7  30715  frgr3vlem1  30754  frgr3vlem2  30755  frgrncvvdeqlem8  30787  frgrncvvdeqlem9  30788  numclwwlk5  30869  frgrreg  30875  frgrregord013  30876  friendshipgt3  30879  isgrpo  30979  vciOLD  31043  vcex  31060  nmogtmnf  31252  siilem1  31333  siii  31335  ajmoi  31340  bcsiALT  31661  hhcms  31685  ocval  31762  hsupval  31816  omlsilem  31884  h1de2bi  32036  h1de2ctlem  32037  hosubeq0i  32308  adjmo  32314  nmopgtmnf  32350  nlfnval  32363  nmcopex  32511  nmcfnex  32535  riesz4i  32545  riesz1  32547  riesz2  32548  opsqrlem1  32622  superpos  32836  hatomistici  32844  chpssati  32845  mdsymlem3  32887  3o1cs  32939  3o2cs  32940  3o3cs  32941  iunrnmptss  33039  brabgaf  33080  f1mptrn  33109  ffsrn  33200  xnn0gt0  33241  hashxpe  33279  elrgspnlem4  33686  mxidlnzrb  33883  evl1deg2  33988  evl1deg3  33989  fedgmul  34142  cos9thpiminplylem2  34294  ordtrest2NEWlem  34433  qqhval2  34493  esumfsup  34581  esumcvg  34597  cntnevol  34740  ddemeas  34748  dya2icoseg2  34790  dya2iocnei  34794  eulerpartlems  34872  eulerpartlemgvv  34888  eulerpart  34894  cndprobprob  34950  ballotlemsdom  35024  ballotth  35050  bnj945  35284  bnj1379  35340  bnj1459  35353  bnj557  35411  bnj571  35416  bnj849  35435  bnj964  35453  bnj978  35459  bnj1018g  35473  bnj1018  35474  bnj1020  35475  bnj1033  35479  bnj1175  35514  bnj1398  35544  bnj1417  35551  bnj1523  35581  nummin  35599  r1omhf  35615  axprALT2  35618  fineqvnttrclselem1  35648  rankkardu  35698  onvf1odlem4  35704  onvf1od  35705  vonf1osev  35710  vonf1oonfo  35713  cusgr3cyclex  35726  txpconn  35812  satfv1  35943  satffun  35989  msubco  36111  mclsax  36149  dfon2lem7  36367  dfon2lem8  36368  pprodss4v  36462  fullfunfv  36527  altxpsspw  36558  funtransport  36612  fvtransport  36613  funray  36721  fvray  36722  funline  36723  fvline  36725  finminlem  36938  bisym1  37039  onsucconni  37057  onsucsuccmpi  37063  weiunse  37088  bj-currypara  37261  bj-cbvaw  37372  axc11n11r  37417  bj-equsal2  37569  bj-xpima1snALT  37702  bj-unexg  37783  bj-bm1.3ii  37809  bj-axseprep  37820  bj-axreprepsep  37821  bj-opelidb1ALT  37919  mptsnunlem  38093  iooelexlt  38117  relowlpssretop  38119  rdgeqoa  38125  difunieq  38129  nlpineqsn  38163  fvineqsneq  38167  wl-ax12v2cl  38261  wl-lem-nexmo  38331  ptrecube  38370  poimirlem26  38396  poimirlem30  38400  poimir  38403  ismblfin  38411  itg2addnclem  38421  dvasin  38454  sdclem2  38493  totbndbnd  38540  ismgmOLD  38601  exidresid  38630  isrngo  38648  rngoablo2  38660  rngoueqz  38691  isdivrngo  38701  isdrngo1  38707  isdrngo2  38709  ispridl2  38789  relcnveq3  39076  elrelscnveq3  39376  disjimeceqim  39553  dmqsblocks  39716  ax12eq  39815  ax12el  39816  lkr0f  39968  hl2at  40279  dalemswapyz  40530  pclfinclN  40824  osumcllem11N  40840  pexmidlem8N  40851  ltrnnid  41010  aks4d1p8  42954  redvmptabs  43236  sn-00id  43277  eu6w  43523  mptfcl  43566  fphpd  43658  elmnc  43978  itgoval  44003  arearect  44057  reabsifpos  44475  clsk3nimkb  44881  grumnud  45111  nanorxor  45130  pm11.71  45222  iotavalsb  45258  sbiota1  45259  2uasbanh  45385  eel0TT  45527  eelT00  45528  eelTTT  45529  eelT11  45530  eelT12  45532  eelTT1  45533  eelT01  45534  eel0T1  45535  eelTT  45594  uunT1p1  45604  uun121  45606  uun121p1  45607  un2122  45613  uunTT1  45616  uunTT1p1  45617  uunTT1p2  45618  uunT11  45619  uunT11p1  45620  uunT11p2  45621  uunT12  45622  uunT12p1  45623  uunT12p2  45624  uunT12p3  45625  uunT12p4  45626  uunT12p5  45627  uun111  45628  3anidm12p2  45630  uun123  45631  3impdirp1  45639  undif3VD  45705  ax6e2ndeqVD  45732  2uasbanhVD  45734  ax6e2ndeqALT  45754  iunconnlem2  45758  sineq0ALT  45760  modelaxreplem1  45802  permaxrep  45830  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  stoweidlem3  46832  stoweidlem17  46846  fourierdlem42  46978  fourierdlem48  46983  fourierdlem50  46985  fourierdlem51  46986  fourierdlem76  47011  fourierdlem83  47018  fourierdlem87  47022  hoidmvval0  47416  evenwodadd  47730  rexrsb  47989  2reu8i  48002  2reuimp  48004  afv0nbfvbi  48040  afvfv0bi  48041  afveu  48042  fnbrafvb  48043  afvres  48061  tz6.12-afv  48062  dmfcoafv  48064  afvco2  48065  aovprc  48077  aovrcl  48078  aovmpt4g  48090  afv2eu  48127  afv2res  48128  tz6.12-afv2  48129  tz6.12i-afv2  48132  afv2rnfveq  48151  fvmptrab  48181  fvmptrabdm  48182  fzopred  48212  2ffzoeq  48217  muldvdsfacm1  48276  elsprel  48376  prproropf1o  48408  reupr  48423  lighneal  48515  odd2prm2  48635  even3prm2  48636  grictr  48840  grlimgrtrilem2  48919  usgrexmpl12ngric  48955  gpgprismgr4cycllem8  49019  gpgprismgr4cycllem11  49022  pgnbgreunbgrlem2lem1  49031  upgrwlkupwlk  49057  islinindfis  49380  rrx2linest  49673  line2ylem  49682  mofeu  49777  homf0  49936  uobffth  50145  uobeqw  50146  initopropd  50170  termopropd  50171  zeroopropd  50172  fucofvalne  50252  isthincd2  50364  lanrcl  50548  ranrcl  50549  setrec2fun  50619  elsetrecslem  50626  setrecsres  50629  secval  50674  cscval  50675  cotval  50676