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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3i  294  ex  417  3expa  1134  3ori  1449  an42ds  1517  nanass  1537  19.38  1866  19.35  1904  19.8aw  2079  sbrimvw  2131  equsexv  2310  sbi2  2343  nfeqf2  2415  equsex  2456  dfmoeu  2569  2mo  2682  axie2  2736  necon1bi  2992  necon1i  2997  r19.35  3129  spc2ed  3569  reu6  3698  rabssrabd  4045  uneqin  4250  difin0ss  4336  inelcm  4431  falseral0OLD  4481  raaan2  4488  difprsn1  4772  tppreqb  4777  n0snor2el  4802  unissint  4941  intminss  4943  dfiun2g  4998  iununi  5069  triin  5239  bm1.3iiOLD  5267  eusv2nf  5367  reusv3i  5376  axprglem  5408  axprg  5409  moabexOLD  5441  opelopabt  5517  eqrelrel  5784  opeliunxp2  5825  opelrn  5934  ssxpb  6173  xpima  6181  xpimasn  6184  dmsn0el  6213  relcnvtr  6270  relcoi2  6279  elsnxp  6293  reuop  6295  iotanul  6517  dffv2  6977  fnfvrnss  7117  fressnfv  7158  fconst5  7205  f1mpt  7260  isocnv3  7331  f1owe  7352  ovprc  7449  fvmpopr2d  7573  onminesb  7792  onminsb  7793  onintrab  7795  onnminsb  7798  ordsuci  7807  onsucuni2  7830  tfindsg2  7858  zfrep6OLD  7952  fo1stres  8012  fo2ndres  8013  bropopvvv  8085  bropfvvvv  8087  frxp  8122  poseq  8154  soseq  8155  opeliunxp2f  8206  mpoxopoveqd  8217  reldmtpos  8230  frrlem4  8286  tfrlem5  8366  tfrlem9  8372  tfr2  8385  rdgsuc  8411  oaordi  8531  oeordi  8573  omopthi  8647  on2recsov  8654  fvmptmap  8879  mptelixpg  8933  ener  8998  domtr  9004  unen  9042  undom  9053  dom0  9093  xpf1o  9127  mapen  9129  pssnn  9153  unfi  9155  ssfi  9157  ensymfib  9168  entrfil  9169  enfii  9170  domtrfil  9176  unxpdomlem3  9218  isinf  9225  frfi  9245  unblem1  9252  fofinf1o  9289  fsuppun  9347  elirrvOLD  9560  inf3lem2  9598  inf3lem5  9601  cantnfp1lem1  9647  cantnfp1lem3  9649  tcmin  9708  setinds  9718  frr2  9732  r1ordg  9750  r1ord  9752  rankr1ai  9770  r1val3  9810  bndrank  9813  unbndrank  9814  rankr1b  9836  rankxplim3  9853  tcrank  9856  xpnum  9937  cardmin2  9985  infxpenlem  9997  fseqen  10011  dfac8clem  10016  alephsson  10084  alephfp  10092  dfac4  10106  kmlem6  10139  kmlem8  10141  kmlem9  10142  cflem  10228  infpssr  10292  fin1a2lem12  10395  axcc4  10423  axcc4dom  10425  ac6s2  10470  zornn0g  10489  cardidg  10532  unsnen  10537  pwcfsdom  10568  cfpwsdom  10569  gchpwdom  10655  r1tskina  10767  intgru  10799  indpi  10892  nqereu  10914  supsrlem  11096  letrii  11335  dfnn3  12247  zaddcl  12634  nn0ind  12691  fnn0ind  12695  ublbneg  12957  nn01to3  12965  infmrp1  13371  fz0  13567  fzo1fzo0n0  13744  elfzom1elp1fzo  13761  fzo0end  13787  elfznelfzo  13802  fzind2  13817  injresinjlem  13819  fleqceilz  13887  nnsinds  14024  nn0sinds  14025  faclbnd4lem1  14329  hashinf  14371  hasheqf1oi  14387  hashgt0elex  14437  hashgt23el  14461  hashfacen  14491  hash2prde  14507  hash2sspr  14526  fun2dmnop0  14541  iswrddm0  14575  swrdnnn0nd  14694  swrdnd0  14695  swrdlsw  14705  pfxn0  14724  pfxnd0  14726  swrdswrdlem  14741  pfxccatin12lem3  14769  pfxccat3  14771  pfxccat3a  14775  swrdccat3blem  14776  cshwsublen  14833  cshwidxmod  14840  repswcshw  14849  cshw1  14859  trclun  15051  dmtrclfv  15055  sgn3da  15138  rediv  15182  imdiv  15189  fsump1i  15820  modfsummods  15845  bpolydiflem  16108  bpoly3  16112  bpoly4  16113  cos1bnd  16243  sinltx  16245  rpnnen2lem1  16270  rpnnen2lem2  16271  rpnnen2lem12  16281  odd2np1  16399  opoe  16421  omoe  16422  opeo  16423  omeo  16424  gcdcllem1  16557  gcdaddmlem  16582  dfgcd2  16604  algfx  16638  lcmledvds  16657  lcmfunsnlem  16699  lcmfun  16703  coprmprod  16719  coprmproddvdslem  16720  odzval  16851  odzdvds  16855  prmreclem5  16980  mul4sq  17014  prmgaplem5  17115  prmgaplem6  17116  imasaddfnlem  17582  mreexexlem4d  17703  joindmss  18433  meetdmss  18447  gictr  19346  cntzval  19391  symg2bas  19463  odfval  19602  efgsfo  19809  efgrelexlemb  19820  dprddomcld  20073  dprdsubg  20096  dprd2da  20114  lssacs  21066  prmidl2  21437  cnfldinv  21522  pzriprnglem7  21606  ocvval  21786  selvval  22240  dmatmul  22623  mdetfval1  22716  mndifsplit  22762  fvmptnn04if  22975  toprntopon  23051  opnnei  23246  ordtbas2  23317  ordtrest2lem  23329  lmmo  23506  fincmp  23519  bwth  23536  txbas  23693  ptcnplem  23747  tx2ndc  23777  hmphtr  23909  fbun  23966  filconn  24009  ptcmplem5  24182  cnextcn  24193  utoptop  24360  ucncn  24410  metust  24684  cfilucfil  24685  elcncf1di  25023  xrhmeo  25074  phtpycc  25119  copco  25146  pcohtpylem  25147  pcopt  25150  pcopt2  25151  ncvsi  25279  ovolval  25601  iunmbl2  25685  itg2splitlem  25876  cpnfval  26060  plyval  26319  fta1  26438  aaliou2b  26471  tayl0  26491  ulmdvlem3  26531  radcnvlem2  26543  dvradcnv  26550  reeff1o  26576  sincosq1lem  26628  sincosq2sgn  26630  sincosq4sgn  26632  sinq12ge0  26639  logrncl  26698  eflog  26707  cxpge0  26814  logb1  26900  atanf  27011  atanbnd  27057  igamf  27181  igamcl  27182  lgsne0  27465  mul2sq  27549  2sqreultblem  27578  pntibnd  27723  ostth  27769  nobdaymin  27912  nocvxminlem  27913  cutlt  28091  norec2ov  28116  addsuniflem  28160  mulsuniflem  28308  oldfib  28536  zmulscld  28556  zseo  28581  z12addscl  28636  mpteleeOLD  29186  axlowdimlem9  29241  axlowdimlem12  29244  axcontlem2  29256  axcontlem12  29266  structgrssvtx  29315  structgrssiedg  29316  lpvtx  29359  nbuhgr  29634  nbumgr  29638  nbuhgr2vtx1edgblem  29642  nbgr0edglem  29647  nbgr1vtx  29649  uvtx01vtx  29688  prcliscplgr  29705  cusgrsizeinds  29743  sizusglecusglem2  29753  uhgrvd00  29825  fusgrregdegfi  29860  rusgr1vtxlem  29878  wlkeq  29924  wlk1walk  29929  uspgr2wlkeq  29936  wlklenvclwlk  29944  wlkreslem  29958  wlkdlem2  29972  wlkdlem4  29974  spthonepeq  30042  cyclnumvtx  30090  clwlkclwwlkflem  30296  clwlkclwwlkfolem  30299  clwlkclwwlkf  30300  clwwisshclwws  30307  clwwlkneq0  30321  3wlkdlem6  30457  eupth2eucrct  30509  eupth2lem1  30510  eupth2lem3lem7  30526  frgr3vlem1  30565  frgr3vlem2  30566  frgrncvvdeqlem8  30598  frgrncvvdeqlem9  30599  numclwwlk5  30680  frgrreg  30686  frgrregord013  30687  friendshipgt3  30690  isgrpo  30790  vciOLD  30854  vcex  30871  nmogtmnf  31063  siilem1  31144  siii  31146  ajmoi  31151  bcsiALT  31472  hhcms  31496  ocval  31573  hsupval  31627  omlsilem  31695  h1de2bi  31847  h1de2ctlem  31848  hosubeq0i  32119  adjmo  32125  nmopgtmnf  32161  nlfnval  32174  nmcopex  32322  nmcfnex  32346  riesz4i  32356  riesz1  32358  riesz2  32359  opsqrlem1  32433  superpos  32647  hatomistici  32655  chpssati  32656  mdsymlem3  32698  3o1cs  32750  3o2cs  32751  3o3cs  32752  iunrnmptss  32851  brabgaf  32892  f1mptrn  32921  ffsrn  33014  xnn0gt0  33055  hashxpe  33093  elrgspnlem4  33506  mxidlnzrb  33707  evl1deg2  33812  evl1deg3  33813  fedgmul  33966  cos9thpiminplylem2  34118  ordtrest2NEWlem  34257  qqhval2  34317  esumfsup  34405  esumcvg  34421  cntnevol  34563  ddemeas  34571  dya2icoseg2  34613  dya2iocnei  34617  eulerpartlems  34695  eulerpartlemgvv  34711  eulerpart  34717  cndprobprob  34773  ballotlemsdom  34847  ballotth  34873  bnj945  35107  bnj1379  35163  bnj1459  35176  bnj557  35234  bnj571  35239  bnj849  35258  bnj964  35276  bnj978  35282  bnj1018g  35296  bnj1018  35297  bnj1020  35298  bnj1033  35302  bnj1175  35337  bnj1398  35367  bnj1417  35374  bnj1523  35404  nummin  35427  r1omhf  35442  axprALT2  35445  fineqvnttrclselem1  35457  onvf1odlem4  35489  onvf1od  35490  vonf1osev  35495  vonf1oonfo  35498  cusgr3cyclex  35527  txpconn  35623  satfv1  35754  satffun  35800  msubco  35922  mclsax  35960  dfon2lem7  36178  dfon2lem8  36179  pprodss4v  36273  fullfunfv  36338  altxpsspw  36368  funtransport  36422  fvtransport  36423  funray  36531  fvray  36532  funline  36533  fvline  36535  finminlem  36718  bisym1  36819  onsucconni  36837  onsucsuccmpi  36843  weiunse  36868  bj-currypara  37041  bj-cbvaw  37152  axc11n11r  37197  bj-equsal2  37349  bj-xpima1snALT  37481  bj-unexg  37562  bj-bm1.3ii  37588  bj-axseprep  37599  bj-axreprepsep  37600  bj-opelidb1ALT  37698  mptsnunlem  37872  iooelexlt  37896  relowlpssretop  37898  rdgeqoa  37904  difunieq  37908  nlpineqsn  37942  fvineqsneq  37946  wl-ax12v2cl  38040  wl-lem-nexmo  38110  matunitlindflem1  38155  ptrecube  38159  poimirlem26  38185  poimirlem30  38189  poimir  38192  ismblfin  38200  itg2addnclem  38210  dvasin  38243  sdclem2  38281  totbndbnd  38328  ismgmOLD  38389  exidresid  38418  isrngo  38436  rngoablo2  38448  rngoueqz  38479  isdivrngo  38489  isdrngo1  38495  isdrngo2  38497  ispridl2  38577  relcnveq3  38866  elrelscnveq3  39166  disjimeceqim  39343  dmqsblocks  39506  ax12eq  39605  ax12el  39606  lkr0f  39758  hl2at  40069  dalemswapyz  40320  pclfinclN  40614  osumcllem11N  40630  pexmidlem8N  40641  ltrnnid  40800  aks4d1p8  42744  redvmptabs  43011  sn-00id  43052  rictr  43180  eu6w  43300  mptfcl  43343  fphpd  43435  elmnc  43755  itgoval  43780  arearect  43834  reabsifpos  44252  clsk3nimkb  44658  grumnud  44888  nanorxor  44907  pm11.71  44999  iotavalsb  45035  sbiota1  45036  2uasbanh  45162  eel0TT  45304  eelT00  45305  eelTTT  45306  eelT11  45307  eelT12  45309  eelTT1  45310  eelT01  45311  eel0T1  45312  eelTT  45371  uunT1p1  45381  uun121  45383  uun121p1  45384  un2122  45390  uunTT1  45393  uunTT1p1  45394  uunTT1p2  45395  uunT11  45396  uunT11p1  45397  uunT11p2  45398  uunT12  45399  uunT12p1  45400  uunT12p2  45401  uunT12p3  45402  uunT12p4  45403  uunT12p5  45404  uun111  45405  3anidm12p2  45407  uun123  45408  3impdirp1  45416  undif3VD  45482  ax6e2ndeqVD  45509  2uasbanhVD  45511  ax6e2ndeqALT  45531  iunconnlem2  45535  sineq0ALT  45537  modelaxreplem1  45579  permaxrep  45607  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  stoweidlem3  46609  stoweidlem17  46623  fourierdlem42  46755  fourierdlem48  46760  fourierdlem50  46762  fourierdlem51  46763  fourierdlem76  46788  fourierdlem83  46795  fourierdlem87  46799  hoidmvval0  47193  evenwodadd  47495  rexrsb  47726  2reu8i  47739  2reuimp  47741  afv0nbfvbi  47777  afvfv0bi  47778  afveu  47779  fnbrafvb  47780  afvres  47798  tz6.12-afv  47799  dmfcoafv  47801  afvco2  47802  aovprc  47814  aovrcl  47815  aovmpt4g  47827  afv2eu  47864  afv2res  47865  tz6.12-afv2  47866  tz6.12i-afv2  47869  afv2rnfveq  47888  fvmptrab  47918  fvmptrabdm  47919  fzopred  47949  2ffzoeq  47954  muldvdsfacm1  48013  elsprel  48113  prproropf1o  48145  reupr  48160  lighneal  48252  odd2prm2  48372  even3prm2  48373  grictr  48577  grlimgrtrilem2  48656  usgrexmpl12ngric  48692  gpgprismgr4cycllem8  48756  gpgprismgr4cycllem11  48759  pgnbgreunbgrlem2lem1  48768  upgrwlkupwlk  48794  ovn0ssdmfun  48813  islinindfis  49114  rrx2linest  49407  line2ylem  49416  mofeu  49511  homf0  49672  uobffth  49881  uobeqw  49882  initopropd  49906  termopropd  49907  zeroopropd  49908  fucofvalne  49988  isthincd2  50100  lanrcl  50284  ranrcl  50285  setrec2fun  50355  elsetrecslem  50362  setrecsres  50365  secval  50410  cscval  50411  cotval  50412