Theorem sylbir 237

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3i  293  ex  415  3expa  1114  3ori  1420  nanass  1499  19.38  1835  19.35  1874  sbi2  2306  sbi2vOLD  2320  nfeqf2  2391  equsex  2436  sbi2ALT  2603  dfmoeu  2614  2mo  2729  axie2  2786  necon1bi  3044  necon1i  3049  r19.35  3341  sbhypf  3552  vtocl2OLD  3562  spc2ed  3601  reu6  3716  rabssrabd  4057  uneqin  4254  difin0ss  4327  inelcm  4413  falseral0  4458  raaan2  4463  difprsn1  4726  tppreqb  4731  n0snor2el  4757  unissint  4892  intminss  4894  iununi  5013  triin  5179  bm1.3ii  5198  eusv2nf  5287  reusv3i  5296  moabex  5343  copsex2g  5376  opelopabt  5411  eqrelrel  5664  opeliunxp2  5703  opelrn  5807  ssxpb  6025  xpima  6033  xpimasn  6036  dmsn0el  6062  relcnvtr  6114  relcoi2  6122  elsnxp  6136  reuop  6138  iotanul  6327  dffv2  6750  fnfvrnss  6878  fressnfv  6916  fconst5  6962  f1mpt  7013  isocnv3  7079  f1owe  7100  ovprc  7188  onminesb  7507  onminsb  7508  onintrab  7510  onnminsb  7513  onsucuni2  7543  tfindsg2  7570  zfrep6  7650  fo1stres  7709  fo2ndres  7710  bropopvvv  7779  bropfvvvv  7781  frxp  7814  opeliunxp2f  7870  mpoxopoveqd  7881  reldmtpos  7894  wfrlem4  7952  wfrlem12  7960  wfrlem16  7964  wfr2  7968  tfrlem5  8010  tfrlem9  8015  tfr2  8028  rdgsuc  8054  oaordi  8166  oeordi  8207  omopthi  8278  fvmptmap  8439  mptelixpg  8493  ener  8550  domtr  8556  snfi  8588  unen  8590  xpf1o  8673  mapen  8675  unxpdomlem3  8718  isinf  8725  frfi  8757  unblem1  8764  unfi  8779  fofinf1o  8793  fsuppun  8846  inf3lem2  9086  inf3lem5  9089  cantnfp1lem1  9135  cantnfp1lem3  9137  tcmin  9177  r1ordg  9201  r1ord  9203  rankr1ai  9221  r1val3  9261  bndrank  9264  unbndrank  9265  rankr1b  9287  rankxplim3  9304  tcrank  9307  xpnum  9374  cardmin2  9421  infxpenlem  9433  fseqen  9447  dfac8clem  9452  alephsson  9520  alephfp  9528  dfac4  9542  kmlem6  9575  kmlem8  9577  kmlem9  9578  infpssr  9724  fin1a2lem12  9827  axcc4  9855  axcc4dom  9857  ac6s2  9902  zornn0g  9921  cardidg  9964  unsnen  9969  pwcfsdom  9999  cfpwsdom  10000  gchpwdom  10086  r1tskina  10198  intgru  10230  indpi  10323  nqereu  10345  supsrlem  10527  letrii  10759  dfnn3  11646  zaddcl  12016  nn0ind  12071  fnn0ind  12075  ublbneg  12327  nn01to3  12335  infmrp1  12731  fz0  12916  fzo1fzo0n0  13082  elfzom1elp1fzo  13098  fzo0end  13123  elfznelfzo  13136  fzind2  13149  injresinjlem  13151  fleqceilz  13216  nnsinds  13350  nn0sinds  13351  faclbnd4lem1  13647  hashinf  13689  hasheqf1oi  13706  hashgt0elex  13756  hashgt23el  13779  hashfacen  13806  hash2prde  13822  hash2sspr  13840  fun2dmnop0  13846  iswrddm0  13882  swrdnnn0nd  14012  swrdnd0  14013  swrdlsw  14023  pfxn0  14042  pfxnd0  14044  swrdswrdlem  14060  pfxccatin12lem3  14088  pfxccat3  14090  pfxccat3a  14094  swrdccat3blem  14095  cshwsublen  14152  cshwidxmod  14159  repswcshw  14168  cshw1  14178  trclun  14368  dmtrclfv  14372  rediv  14484  imdiv  14491  sqrt0  14595  fsump1i  15118  modfsummods  15142  bpolydiflem  15402  bpoly3  15406  bpoly4  15407  cos1bnd  15534  sinltx  15536  rpnnen2lem1  15561  rpnnen2lem2  15562  rpnnen2lem12  15572  odd2np1  15684  opoe  15706  omoe  15707  opeo  15708  omeo  15709  gcdcllem1  15842  gcdaddmlem  15866  dfgcd2  15888  algfx  15918  lcmledvds  15937  lcmfunsnlem  15979  lcmfun  15983  coprmprod  15999  coprmproddvdslem  16000  odzval  16122  odzdvds  16126  prmreclem5  16250  mul4sq  16284  prmgaplem5  16385  prmgaplem6  16386  imasaddfnlem  16795  mreexexlem4d  16912  joindmss  17611  meetdmss  17625  gictr  18409  cntzval  18445  symg2bas  18515  odfval  18654  efgsfo  18859  efgrelexlemb  18870  dprddomcld  19117  dprdsubg  19140  dprd2da  19158  lssacs  19733  selvval  20325  cnfldinv  20570  ocvval  20805  dmatmul  21100  mdetfval1  21193  mndifsplit  21239  fvmptnn04if  21451  toprntopon  21527  opnnei  21722  ordtbas2  21793  ordtrest2lem  21805  lmmo  21982  fincmp  21995  bwth  22012  txbas  22169  ptcnplem  22223  tx2ndc  22253  hmphtr  22385  fbun  22442  filconn  22485  ptcmplem5  22658  cnextcn  22669  utoptop  22837  ucncn  22888  metust  23162  cfilucfil  23163  elcncf1di  23497  xrhmeo  23544  phtpycc  23589  copco  23616  pcohtpylem  23617  pcopt  23620  pcopt2  23621  ncvsi  23749  ovolval  24068  iunmbl2  24152  itg2splitlem  24343  cpnfval  24523  plyval  24777  fta1  24891  aaliou2b  24924  tayl0  24944  ulmdvlem3  24984  radcnvlem2  24996  dvradcnv  25003  reeff1o  25029  sincosq1lem  25077  sincosq2sgn  25079  sincosq4sgn  25081  sinq12ge0  25088  logrncl  25145  eflog  25154  cxpge0  25260  logb1  25341  atanf  25452  atanbnd  25498  igamf  25622  igamcl  25623  lgsne0  25905  mul2sq  25989  2sqreultblem  26018  pntibnd  26163  ostth  26209  mptelee  26675  axlowdimlem9  26730  axlowdimlem12  26733  axcontlem2  26745  axcontlem12  26755  structgrssvtx  26803  structgrssiedg  26804  lpvtx  26847  nbuhgr  27119  nbumgr  27123  nbuhgr2vtx1edgblem  27127  nbgr0vtxlem  27131  nbgr1vtx  27134  uvtx01vtx  27173  prcliscplgr  27190  cusgrsizeinds  27228  sizusglecusglem2  27238  uhgrvd00  27310  fusgrregdegfi  27345  rusgr1vtxlem  27363  wlkeq  27409  wlk1walk  27414  uspgr2wlkeq  27421  wlklenvclwlk  27430  wlklenvclwlkOLD  27431  wlkreslem  27445  wlkdlem2  27459  wlkdlem4  27461  spthonepeq  27527  clwlkclwwlkflem  27776  clwlkclwwlkfolem  27779  clwlkclwwlkf  27780  clwwisshclwws  27787  clwwlkneq0  27801  3wlkdlem6  27938  eupth2eucrct  27990  eupth2lem1  27991  eupth2lem3lem7  28007  frgr3vlem1  28046  frgr3vlem2  28047  frgrncvvdeqlem8  28079  frgrncvvdeqlem9  28080  numclwwlk5  28161  frgrreg  28167  frgrregord013  28168  friendshipgt3  28171  isgrpo  28268  vciOLD  28332  vcex  28349  nmogtmnf  28541  siilem1  28622  siii  28624  ajmoi  28629  bcsiALT  28950  hhcms  28974  ocval  29051  hsupval  29105  omlsilem  29173  h1de2bi  29325  h1de2ctlem  29326  hosubeq0i  29597  adjmo  29603  nmopgtmnf  29639  nlfnval  29652  nmcopex  29800  nmcfnex  29824  riesz4i  29834  riesz1  29836  riesz2  29837  opsqrlem1  29911  superpos  30125  hatomistici  30133  chpssati  30134  mdsymlem3  30176  3o1cs  30221  3o2cs  30222  3o3cs  30223  iunrnmptss  30311  brabgaf  30353  f1mptrn  30374  ffsrn  30459  fpwrelmap  30463  xnn0gt0  30488  hashxpe  30523  prmidl2  30953  mxidlnzrb  30976  fedgmul  31022  ordtrest2NEWlem  31160  qqhval2  31218  esumfsup  31324  esumcvg  31340  cntnevol  31482  ddemeas  31490  dya2icoseg2  31531  dya2iocnei  31535  eulerpartlems  31613  eulerpartlemgvv  31629  eulerpart  31635  cndprobprob  31691  ballotlemsdom  31764  ballotth  31790  sgn3da  31794  bnj945  32040  bnj1379  32097  bnj1459  32110  bnj557  32168  bnj571  32173  bnj849  32192  bnj964  32210  bnj978  32216  bnj1018g  32230  bnj1018  32231  bnj1020  32232  bnj1033  32236  bnj1175  32271  bnj1398  32301  bnj1417  32308  bnj1523  32338  cusgr3cyclex  32378  txpconn  32474  satfv1  32605  satffun  32651  msubco  32773  mclsax  32811  setinds  33018  dfon2lem7  33029  dfon2lem8  33030  poseq  33090  soseq  33091  frrlem4  33121  frr2  33140  nocvxminlem  33242  nocvxmin  33243  pprodss4v  33340  fullfunfv  33403  altxpsspw  33433  funtransport  33487  fvtransport  33488  funray  33596  fvray  33597  funline  33598  fvline  33600  finminlem  33661  bisym1  33762  onsucconni  33780  onsucsuccmpi  33786  bj-currypara  33890  bj-alcomexcom  34009  axc11n11r  34012  bj-equsal2  34143  bj-xpima1snALT  34264  bj-bm1.3ii  34351  bj-opelidb1ALT  34452  mptsnunlem  34613  iooelexlt  34637  relowlpssretop  34639  rdgeqoa  34645  difunieq  34649  nlpineqsn  34683  fvineqsneq  34687  wl-lem-nexmo  34797  matunitlindflem1  34882  ptrecube  34886  poimirlem26  34912  poimirlem30  34916  poimir  34919  ismblfin  34927  itg2addnclem  34937  dvasin  34972  sdclem2  35011  totbndbnd  35061  ismgmOLD  35122  exidresid  35151  isrngo  35169  rngoablo2  35181  rngoueqz  35212  isdivrngo  35222  isdrngo1  35228  isdrngo2  35230  ispridl2  35310  relcnveq3  35572  elrelscnveq3  35725  ax12eq  36071  ax12el  36072  lkr0f  36224  hl2at  36535  dalemswapyz  36786  pclfinclN  37080  osumcllem11N  37096  pexmidlem8N  37107  ltrnnid  37266  sn-00id  39224  mptfcl  39310  fphpd  39406  elmnc  39729  itgoval  39754  arearect  39815  clsk3nimkb  40383  grumnud  40615  nanorxor  40630  pm11.71  40722  iotavalsb  40758  sbiota1  40759  2uasbanh  40888  eel0TT  41031  eelT00  41032  eelTTT  41033  eelT11  41034  eelT12  41036  eelTT1  41037  eelT01  41038  eel0T1  41039  eelTT  41098  uunT1p1  41108  uun121  41110  uun121p1  41111  un2122  41117  uunTT1  41120  uunTT1p1  41121  uunTT1p2  41122  uunT11  41123  uunT11p1  41124  uunT11p2  41125  uunT12  41126  uunT12p1  41127  uunT12p2  41128  uunT12p3  41129  uunT12p4  41130  uunT12p5  41131  uun111  41132  3anidm12p2  41134  uun123  41135  3impdirp1  41143  undif3VD  41209  ax6e2ndeqVD  41236  2uasbanhVD  41238  ax6e2ndeqALT  41258  iunconnlem2  41262  sineq0ALT  41264  ioodvbdlimc1lem2  42210  ioodvbdlimc2lem  42212  stoweidlem3  42282  stoweidlem17  42296  fourierdlem42  42428  fourierdlem48  42433  fourierdlem50  42435  fourierdlem51  42436  fourierdlem76  42461  fourierdlem83  42468  fourierdlem87  42472  hoidmvval0  42863  rexrsb  43292  2reu8i  43306  2reuimp  43308  afv0nbfvbi  43344  afvfv0bi  43345  afveu  43346  fnbrafvb  43347  afvres  43365  tz6.12-afv  43366  dmfcoafv  43368  afvco2  43369  aovprc  43381  aovrcl  43382  aovmpt4g  43394  afv2eu  43431  afv2res  43432  tz6.12-afv2  43433  tz6.12i-afv2  43436  afv2rnfveq  43455  fvmptrab  43485  fvmptrabdm  43486  fzopred  43516  2ffzoeq  43522  ichan  43624  elsprel  43631  prproropf1o  43663  reupr  43678  lighneal  43770  odd2prm2  43877  even3prm2  43878  upgrwlkupwlk  44009  ovn0ssdmfun  44028  islinindfis  44498  rrx2linest  44723  line2ylem  44732  setrec2fun  44789  elsetrecslem  44795  setrecsres  44798  secval  44840  cscval  44841  cotval  44842