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  2303  sbi2  2336  nfeqf2  2407  equsex  2448  dfmoeu  2561  2mo  2674  axie2  2728  necon1bi  2984  necon1i  2989  r19.35  3121  spc2ed  3556  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  eusv2nf  5357  reusv3i  5366  axprglem  5394  axprg  5395  moabexOLD  5427  opelopabt  5506  eqrelrel  5773  opeliunxp2  5815  opelrn  5925  ssxpb  6166  xpima  6174  xpimasn  6177  dmsn0el  6212  relcnvtrOLD  6270  relcoi2  6280  elsnxp  6294  reuop  6296  iotanul  6518  dffv2  6980  fnfvrnss  7121  fressnfv  7164  fconst5  7212  f1mpt  7265  isocnv3  7340  f1owe  7361  f1oweOLD  7362  ovprc  7458  fvmpopr2d  7582  ovn0ssdmfun  7589  onminesb  7807  onminsb  7808  onintrab  7810  onnminsb  7813  ordsuci  7822  onsucuni2  7845  tfindsg2  7873  zfrep6OLD  7967  fo1stres  8027  fo2ndres  8028  bropopvvv  8101  bropfvvvv  8103  frxp  8138  poseq  8175  soseq  8176  opeliunxp2f  8227  mpoxopoveqd  8238  reldmtpos  8251  frrlem4  8307  tfrlem5  8387  tfrlem9  8393  tfr2  8406  rdgsuc  8432  oaordi  8554  oeordi  8596  omopthi  8670  on2recsov  8677  fvmptmap  8909  mptelixpg  8963  ener  9028  domtr  9034  unen  9073  undom  9084  dom0  9124  xpf1o  9158  mapen  9160  pssnn  9184  unfi  9186  ssfi  9188  ensymfib  9199  entrfil  9200  enfii  9201  domtrfil  9207  unxpdomlem3  9249  isinf  9256  frfi  9276  unblem1  9284  fofinf1o  9321  fsuppun  9379  elirrvOLD  9592  inf3lem2  9630  inf3lem5  9633  cantnfp1lem1  9679  cantnfp1lem3  9681  tcmin  9740  setinds  9750  frr2  9764  r1ordg  9785  r1ord  9787  rankr1ai  9806  r1val3  9850  bndrank  9854  unbndrank  9855  rankr1b  9881  rankxplim3  9898  tcrank  9901  setrec2fun  9973  xpnum  10032  cardmin2  10080  infxpenlem  10092  fseqen  10106  dfac8clem  10111  alephsson  10179  alephfp  10187  dfac4  10201  kmlem6  10234  kmlem8  10236  kmlem9  10237  cflem  10323  infpssr  10386  fin1a2lem12  10489  axcc4  10517  axcc4dom  10519  ac6s2  10564  zornn0g  10583  cardidg  10632  unsnen  10637  pwcfsdom  10668  cfpwsdom  10669  gchpwdom  10755  r1tskina  10867  intgru  10899  indpi  10992  nqereu  11014  supsrlem  11196  letrii  11435  dfnn3  12349  zaddcl  12736  nn0ind  12794  fnn0ind  12798  ublbneg  13060  nn01to3  13068  infmrp1  13475  fz0  13672  fzo1fzo0n0  13850  elfzom1elp1fzo  13867  fzo0end  13893  elfznelfzo  13908  fzind2  13923  injresinjlem  13925  fleqceilz  13994  nnsinds  14131  nn0sinds  14132  faclbnd4lem1  14437  hashinf  14479  hasheqf1oi  14495  hashgt0elex  14545  hashgt23el  14569  hashfacen  14599  hash2prde  14615  hash2sspr  14634  fun2dmnop0  14649  iswrddm0  14683  swrdnnn0nd  14806  swrdnd0  14807  swrdlsw  14817  pfxn0  14836  pfxnd0  14838  swrdswrdlem  14853  pfxccatin12lem3  14881  pfxccat3  14883  pfxccat3a  14887  swrdccat3blem  14888  cshwsublen  14947  cshwidxmod  14954  repswcshw  14963  cshw1  14973  trclun  15167  dmtrclfv  15171  sgn3da  15254  rediv  15298  imdiv  15305  fsump1i  15935  modfsummods  15960  bpolydiflem  16220  bpoly3  16224  bpoly4  16225  cos1bnd  16355  sinltx  16357  rpnnen2lem1  16382  rpnnen2lem2  16383  rpnnen2lem12  16393  odd2np1  16511  opoe  16533  omoe  16534  opeo  16535  omeo  16536  gcdcllem1  16669  gcdaddmlem  16696  dfgcd2  16719  algfx  16755  lcmledvds  16774  lcmfunsnlem  16816  lcmfun  16820  coprmprod  16836  coprmproddvdslem  16837  odzval  16969  odzdvds  16973  prmreclem5  17098  mul4sq  17132  prmgaplem5  17233  prmgaplem6  17234  imasaddfnlem  17700  mreexexlem4d  17821  joindmss  18551  meetdmss  18565  gictr  19490  cntzval  19535  symg2bas  19607  odfval  19746  efgsfo  19953  efgrelexlemb  19964  dprddomcld  20217  dprdsubg  20240  dprd2da  20258  rictr  20752  isdrng3lem1  21005  isdrng3  21007  lssacs  21242  prmidl2  21622  cnfldinv  21709  pzriprnglem7  21793  ocvval  21973  selvval  22429  dmatmul  22812  mdetfval1  22905  mndifsplit  22951  matunitlindflem1  22994  fvmptnn04if  23167  toprntopon  23243  opnnei  23438  ordtbas2  23509  ordtrest2lem  23521  lmmo  23698  fincmp  23711  bwth  23728  txbas  23886  ptcnplem  23940  tx2ndc  23970  hmphtr  24102  fbun  24159  filconn  24202  ptcmplem5  24375  cnextcn  24386  utoptop  24553  ucncn  24603  metust  24877  cfilucfil  24878  elcncf1di  25216  xrhmeo  25267  phtpycc  25312  copco  25339  pcohtpylem  25340  pcopt  25343  pcopt2  25344  ncvsi  25472  ovolval  25794  iunmbl2  25878  itg2splitlem  26069  cpnfval  26252  plyval  26511  fta1  26629  aaliou2b  26668  tayl0  26689  ulmdvlem3  26729  radcnvlem2  26741  dvradcnv  26748  reeff1o  26774  sincosq1lem  26826  sincosq2sgn  26828  sincosq4sgn  26830  sinq12ge0  26837  logrncl  26895  eflog  26904  cxpge0  27011  logb1  27097  atanf  27208  atanbnd  27254  igamf  27378  igamcl  27379  lgsne0  27662  mul2sq  27746  2sqreultblem  27775  pntibnd  27920  ostth  27966  nobdaymin  28139  nocvxminlem  28140  cutlt  28318  norec2ov  28343  addsuniflem  28387  mulsuniflem  28535  oldfib  28763  zmulscld  28783  zseo  28808  z12addscl  28863  mpteleeOLD  29473  axlowdimlem9  29528  axlowdimlem12  29531  axcontlem2  29543  axcontlem12  29553  structgrssvtx  29602  structgrssiedg  29603  lpvtx  29646  nbuhgr  29924  nbumgr  29928  nbuhgr2vtx1edgblem  29932  nbgr0edglem  29937  nbgr1vtx  29939  uvtx01vtx  29978  prcliscplgr  29995  cusgrsizeinds  30033  sizusglecusglem2  30043  uhgrvd00  30115  fusgrregdegfi  30150  rusgr1vtxlem  30168  wlkeq  30214  wlk1walk  30219  uspgr2wlkeq  30226  wlklenvclwlk  30234  wlkreslem  30248  wlkdlem2  30262  wlkdlem4  30264  spthonepeq  30338  cyclnumvtx  30388  clwlkclwwlkflem  30595  clwlkclwwlkfolem  30598  clwlkclwwlkf  30599  clwwisshclwws  30606  clwwlkneq0  30620  3wlkdlem6  30766  eupth2eucrct  30818  eupth2lem1  30819  eupth2lem3lem7  30835  frgr3vlem1  30874  frgr3vlem2  30875  frgrncvvdeqlem8  30907  frgrncvvdeqlem9  30908  numclwwlk5  30989  frgrreg  30995  frgrregord013  30996  friendshipgt3  30999  isgrpo  31099  vciOLD  31163  vcex  31180  nmogtmnf  31372  siilem1  31453  siii  31455  ajmoi  31460  bcsiALT  31781  hhcms  31805  ocval  31882  hsupval  31936  omlsilem  32004  h1de2bi  32156  h1de2ctlem  32157  hosubeq0i  32428  adjmo  32434  nmopgtmnf  32470  nlfnval  32483  nmcopex  32631  nmcfnex  32655  riesz4i  32665  riesz1  32667  riesz2  32668  opsqrlem1  32742  superpos  32956  hatomistici  32964  chpssati  32965  mdsymlem3  33007  3o1cs  33059  3o2cs  33060  3o3cs  33061  iunrnmptss  33159  brabgaf  33200  f1mptrn  33229  ffsrn  33320  xnn0gt0  33361  hashxpe  33399  elrgspnlem4  33806  mxidlnzrb  34004  evl1deg2  34109  evl1deg3  34110  fedgmul  34263  cos9thpiminplylem2  34415  ordtrest2NEWlem  34554  qqhval2  34614  esumfsup  34702  esumcvg  34718  cntnevol  34861  ddemeas  34869  dya2icoseg2  34910  dya2iocnei  34914  eulerpartlems  34992  eulerpartlemgvv  35008  eulerpart  35014  cndprobprob  35070  ballotlemsdom  35144  ballotth  35170  bnj945  35404  bnj1379  35460  bnj1459  35473  bnj557  35531  bnj571  35536  bnj849  35555  bnj964  35573  bnj978  35579  bnj1018g  35593  bnj1018  35594  bnj1020  35595  bnj1033  35599  bnj1175  35634  bnj1398  35664  bnj1417  35671  bnj1523  35701  nummin  35722  r1omfi  35730  axprALT2  35734  werankwe  35739  fineqvnttrclselem1  35789  rankkardu  35839  onvf1odlem4  35885  onvf1od  35886  vonf1osev  35891  onprcf1acwevdlem2  35896  vonf1oonfo  35898  cusgr3cyclex  35911  txpconn  35997  satfv1  36128  satffun  36174  msubco  36296  mclsax  36334  dfon2lem7  36551  dfon2lem8  36552  pprodss4v  36646  fullfunfv  36711  altxpsspw  36742  funtransport  36796  fvtransport  36797  funray  36905  fvray  36906  funline  36907  fvline  36909  finminlem  37106  bisym1  37207  onsucconni  37225  onsucsuccmpi  37231  weiunse  37256  bj-currypara  37429  bj-cbvaw  37540  axc11n11r  37585  bj-equsal2  37737  bj-xpima1snALT  37870  bj-unexg  37951  bj-bm1.3ii  37979  bj-axseprep  37990  bj-axreprepsep  37991  bj-opelidb1ALT  38087  mptsnunlem  38261  iooelexlt  38285  relowlpssretop  38287  rdgeqoa  38293  difunieq  38297  nlpineqsn  38331  fvineqsneq  38335  wl-ax12v2cl  38429  wl-lem-nexmo  38499  ptrecube  38538  poimirlem26  38564  poimirlem30  38568  poimir  38571  ismblfin  38579  itg2addnclem  38589  dvasin  38622  sdclem2  38676  totbndbnd  38723  ismgmOLD  38784  exidresid  38813  isrngo  38831  rngoablo2  38843  rngoueqz  38874  isdivrngo  38884  isdrngo1  38890  isdrngo2  38892  ispridl2  38972  relcnveq3  39259  elrelscnveq3  39559  disjimeceqim  39736  dmqsblocks  39899  ax12eq  39998  ax12el  39999  lkr0f  40151  hl2at  40462  dalemswapyz  40713  pclfinclN  41007  osumcllem11N  41023  pexmidlem8N  41034  ltrnnid  41193  aks4d1p8  43137  redvmptabs  43411  sn-00id  43452  eu6w  43687  mptfcl  43730  fphpd  43822  elmnc  44137  itgoval  44162  arearect  44216  reabsifpos  44633  clsk3nimkb  45039  grumnud  45269  nanorxor  45288  pm11.71  45380  iotavalsb  45416  sbiota1  45417  2uasbanh  45543  eel0TT  45685  eelT00  45686  eelTTT  45687  eelT11  45688  eelT12  45690  eelTT1  45691  eelT01  45692  eel0T1  45693  eelTT  45752  uunT1p1  45762  uun121  45764  uun121p1  45765  un2122  45771  uunTT1  45774  uunTT1p1  45775  uunTT1p2  45776  uunT11  45777  uunT11p1  45778  uunT11p2  45779  uunT12  45780  uunT12p1  45781  uunT12p2  45782  uunT12p3  45783  uunT12p4  45784  uunT12p5  45785  uun111  45786  3anidm12p2  45788  uun123  45789  3impdirp1  45797  undif3VD  45863  ax6e2ndeqVD  45890  2uasbanhVD  45892  ax6e2ndeqALT  45912  iunconnlem2  45916  sineq0ALT  45918  modelaxreplem1  45967  permaxrep  45995  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  stoweidlem3  47012  stoweidlem17  47026  fourierdlem42  47158  fourierdlem48  47163  fourierdlem50  47165  fourierdlem51  47166  fourierdlem76  47191  fourierdlem83  47198  fourierdlem87  47202  hoidmvval0  47596  evenwodadd  47910  rexrsb  48169  2reu8i  48182  2reuimp  48184  afv0nbfvbi  48220  afvfv0bi  48221  afveu  48222  fnbrafvb  48223  afvres  48241  tz6.12-afv  48242  dmfcoafv  48244  afvco2  48245  aovprc  48257  aovrcl  48258  aovmpt4g  48270  afv2eu  48307  afv2res  48308  tz6.12-afv2  48309  tz6.12i-afv2  48312  afv2rnfveq  48331  fvmptrab  48361  fvmptrabdm  48362  fzopred  48392  2ffzoeq  48397  muldvdsfacm1  48456  elsprel  48556  prproropf1o  48588  reupr  48603  lighneal  48695  odd2prm2  48815  even3prm2  48816  grictr  49020  grlimgrtrilem2  49099  usgrexmpl12ngric  49135  gpgprismgr4cycllem8  49199  gpgprismgr4cycllem11  49202  pgnbgreunbgrlem2lem1  49211  upgrwlkupwlk  49237  islinindfis  49560  rrx2linest  49853  line2ylem  49862  mofeu  49957  homf0  50116  uobffth  50325  uobeqw  50326  initopropd  50350  termopropd  50351  zeroopropd  50352  fucofvalne  50432  isthincd2  50544  lanrcl  50728  ranrcl  50729  elsetrecslem  50791  setrecsres  50794  secval  50839  cscval  50840  cotval  50841