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  1500  19.38  1839  19.35  1878  sbi2  2310  sbi2vOLD  2324  nfeqf2  2395  equsex  2440  sbi2ALT  2607  dfmoeu  2618  2mo  2733  axie2  2788  necon1bi  3044  necon1i  3049  r19.35  3341  sbhypf  3552  vtocl2OLD  3562  spc2ed  3602  reu6  3717  rabssrabd  4058  uneqin  4255  difin0ss  4328  inelcm  4414  falseral0  4459  raaan2  4464  difprsn1  4733  tppreqb  4738  n0snor2el  4764  unissint  4900  intminss  4902  iununi  5021  triin  5187  bm1.3ii  5206  eusv2nf  5296  reusv3i  5305  moabex  5351  copsex2g  5384  opelopabt  5419  eqrelrel  5670  opeliunxp2  5709  opelrn  5813  ssxpb  6031  xpima  6039  xpimasn  6042  dmsn0el  6068  relcnvtr  6120  relcoi2  6128  elsnxp  6142  reuop  6144  iotanul  6333  dffv2  6756  fnfvrnss  6884  fressnfv  6922  fconst5  6968  f1mpt  7019  isocnv3  7085  f1owe  7106  ovprc  7194  onminesb  7513  onminsb  7514  onintrab  7516  onnminsb  7519  onsucuni2  7549  tfindsg2  7576  zfrep6  7656  fo1stres  7715  fo2ndres  7716  bropopvvv  7785  bropfvvvv  7787  frxp  7820  opeliunxp2f  7876  mpoxopoveqd  7887  reldmtpos  7900  wfrlem4  7958  wfrlem12  7966  wfrlem16  7970  wfr2  7974  tfrlem5  8016  tfrlem9  8021  tfr2  8034  rdgsuc  8060  oaordi  8172  oeordi  8213  omopthi  8284  fvmptmap  8445  mptelixpg  8499  ener  8556  domtr  8562  snfi  8594  unen  8596  xpf1o  8679  mapen  8681  unxpdomlem3  8724  isinf  8731  frfi  8763  unblem1  8770  unfi  8785  fofinf1o  8799  fsuppun  8852  inf3lem2  9092  inf3lem5  9095  cantnfp1lem1  9141  cantnfp1lem3  9143  tcmin  9183  r1ordg  9207  r1ord  9209  rankr1ai  9227  r1val3  9267  bndrank  9270  unbndrank  9271  rankr1b  9293  rankxplim3  9310  tcrank  9313  xpnum  9380  cardmin2  9427  infxpenlem  9439  fseqen  9453  dfac8clem  9458  alephsson  9526  alephfp  9534  dfac4  9548  kmlem6  9581  kmlem8  9583  kmlem9  9584  infpssr  9730  fin1a2lem12  9833  axcc4  9861  axcc4dom  9863  ac6s2  9908  zornn0g  9927  cardidg  9970  unsnen  9975  pwcfsdom  10005  cfpwsdom  10006  gchpwdom  10092  r1tskina  10204  intgru  10236  indpi  10329  nqereu  10351  supsrlem  10533  letrii  10765  dfnn3  11652  zaddcl  12023  nn0ind  12078  fnn0ind  12082  ublbneg  12334  nn01to3  12342  infmrp1  12738  fz0  12923  fzo1fzo0n0  13089  elfzom1elp1fzo  13105  fzo0end  13130  elfznelfzo  13143  fzind2  13156  injresinjlem  13158  fleqceilz  13223  nnsinds  13357  nn0sinds  13358  faclbnd4lem1  13654  hashinf  13696  hasheqf1oi  13713  hashgt0elex  13763  hashgt23el  13786  hashfacen  13813  hash2prde  13829  hash2sspr  13847  fun2dmnop0  13853  iswrddm0  13888  swrdnnn0nd  14018  swrdnd0  14019  swrdlsw  14029  pfxn0  14048  pfxnd0  14050  swrdswrdlem  14066  pfxccatin12lem3  14094  pfxccat3  14096  pfxccat3a  14100  swrdccat3blem  14101  cshwsublen  14158  cshwidxmod  14165  repswcshw  14174  cshw1  14184  trclun  14374  dmtrclfv  14378  rediv  14490  imdiv  14497  sqrt0  14601  fsump1i  15124  modfsummods  15148  bpolydiflem  15408  bpoly3  15412  bpoly4  15413  cos1bnd  15540  sinltx  15542  rpnnen2lem1  15567  rpnnen2lem2  15568  rpnnen2lem12  15578  odd2np1  15690  opoe  15712  omoe  15713  opeo  15714  omeo  15715  gcdcllem1  15848  gcdaddmlem  15872  dfgcd2  15894  algfx  15924  lcmledvds  15943  lcmfunsnlem  15985  lcmfun  15989  coprmprod  16005  coprmproddvdslem  16006  odzval  16128  odzdvds  16132  prmreclem5  16256  mul4sq  16290  prmgaplem5  16391  prmgaplem6  16392  imasaddfnlem  16801  mreexexlem4d  16918  joindmss  17617  meetdmss  17631  gictr  18415  cntzval  18451  symg2bas  18521  odfval  18660  efgsfo  18865  efgrelexlemb  18876  dprddomcld  19123  dprdsubg  19146  dprd2da  19164  lssacs  19739  selvval  20331  cnfldinv  20576  ocvval  20811  dmatmul  21106  mdetfval1  21199  mndifsplit  21245  fvmptnn04if  21457  toprntopon  21533  opnnei  21728  ordtbas2  21799  ordtrest2lem  21811  lmmo  21988  fincmp  22001  bwth  22018  txbas  22175  ptcnplem  22229  tx2ndc  22259  hmphtr  22391  fbun  22448  filconn  22491  ptcmplem5  22664  cnextcn  22675  utoptop  22843  ucncn  22894  metust  23168  cfilucfil  23169  elcncf1di  23503  xrhmeo  23550  phtpycc  23595  copco  23622  pcohtpylem  23623  pcopt  23626  pcopt2  23627  ncvsi  23755  ovolval  24074  iunmbl2  24158  itg2splitlem  24349  cpnfval  24529  plyval  24783  fta1  24897  aaliou2b  24930  tayl0  24950  ulmdvlem3  24990  radcnvlem2  25002  dvradcnv  25009  reeff1o  25035  sincosq1lem  25083  sincosq2sgn  25085  sincosq4sgn  25087  sinq12ge0  25094  logrncl  25151  eflog  25160  cxpge0  25266  logb1  25347  atanf  25458  atanbnd  25504  igamf  25628  igamcl  25629  lgsne0  25911  mul2sq  25995  2sqreultblem  26024  pntibnd  26169  ostth  26215  mptelee  26681  axlowdimlem9  26736  axlowdimlem12  26739  axcontlem2  26751  axcontlem12  26761  structgrssvtx  26809  structgrssiedg  26810  lpvtx  26853  nbuhgr  27125  nbumgr  27129  nbuhgr2vtx1edgblem  27133  nbgr0vtxlem  27137  nbgr1vtx  27140  uvtx01vtx  27179  prcliscplgr  27196  cusgrsizeinds  27234  sizusglecusglem2  27244  uhgrvd00  27316  fusgrregdegfi  27351  rusgr1vtxlem  27369  wlkeq  27415  wlk1walk  27420  uspgr2wlkeq  27427  wlklenvclwlk  27436  wlklenvclwlkOLD  27437  wlkreslem  27451  wlkdlem2  27465  wlkdlem4  27467  spthonepeq  27533  clwlkclwwlkflem  27782  clwlkclwwlkfolem  27785  clwlkclwwlkf  27786  clwwisshclwws  27793  clwwlkneq0  27807  3wlkdlem6  27944  eupth2eucrct  27996  eupth2lem1  27997  eupth2lem3lem7  28013  frgr3vlem1  28052  frgr3vlem2  28053  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  numclwwlk5  28167  frgrreg  28173  frgrregord013  28174  friendshipgt3  28177  isgrpo  28274  vciOLD  28338  vcex  28355  nmogtmnf  28547  siilem1  28628  siii  28630  ajmoi  28635  bcsiALT  28956  hhcms  28980  ocval  29057  hsupval  29111  omlsilem  29179  h1de2bi  29331  h1de2ctlem  29332  hosubeq0i  29603  adjmo  29609  nmopgtmnf  29645  nlfnval  29658  nmcopex  29806  nmcfnex  29830  riesz4i  29840  riesz1  29842  riesz2  29843  opsqrlem1  29917  superpos  30131  hatomistici  30139  chpssati  30140  mdsymlem3  30182  3o1cs  30227  3o2cs  30228  3o3cs  30229  iunrnmptss  30317  brabgaf  30359  f1mptrn  30380  ffsrn  30465  fpwrelmap  30469  xnn0gt0  30494  hashxpe  30529  prmidl2  30958  mxidlnzrb  30981  fedgmul  31027  ordtrest2NEWlem  31165  qqhval2  31223  esumfsup  31329  esumcvg  31345  cntnevol  31487  ddemeas  31495  dya2icoseg2  31536  dya2iocnei  31540  eulerpartlems  31618  eulerpartlemgvv  31634  eulerpart  31640  cndprobprob  31696  ballotlemsdom  31769  ballotth  31795  sgn3da  31799  bnj945  32045  bnj1379  32102  bnj1459  32115  bnj557  32173  bnj571  32178  bnj849  32197  bnj964  32215  bnj978  32221  bnj1018g  32235  bnj1018  32236  bnj1020  32237  bnj1033  32241  bnj1175  32276  bnj1398  32306  bnj1417  32313  bnj1523  32343  cusgr3cyclex  32383  txpconn  32479  satfv1  32610  satffun  32656  msubco  32778  mclsax  32816  setinds  33023  dfon2lem7  33034  dfon2lem8  33035  poseq  33095  soseq  33096  frrlem4  33126  frr2  33145  nocvxminlem  33247  nocvxmin  33248  pprodss4v  33345  fullfunfv  33408  altxpsspw  33438  funtransport  33492  fvtransport  33493  funray  33601  fvray  33602  funline  33603  fvline  33605  finminlem  33666  bisym1  33767  onsucconni  33785  onsucsuccmpi  33791  bj-currypara  33895  bj-alcomexcom  34014  axc11n11r  34017  bj-equsal2  34148  bj-xpima1snALT  34272  bj-bm1.3ii  34360  bj-opelidb1ALT  34461  mptsnunlem  34622  iooelexlt  34646  relowlpssretop  34648  rdgeqoa  34654  difunieq  34658  nlpineqsn  34692  fvineqsneq  34696  wl-lem-nexmo  34818  matunitlindflem1  34903  ptrecube  34907  poimirlem26  34933  poimirlem30  34937  poimir  34940  ismblfin  34948  itg2addnclem  34958  dvasin  34993  sdclem2  35032  totbndbnd  35082  ismgmOLD  35143  exidresid  35172  isrngo  35190  rngoablo2  35202  rngoueqz  35233  isdivrngo  35243  isdrngo1  35249  isdrngo2  35251  ispridl2  35331  relcnveq3  35593  elrelscnveq3  35746  ax12eq  36092  ax12el  36093  lkr0f  36245  hl2at  36556  dalemswapyz  36807  pclfinclN  37101  osumcllem11N  37117  pexmidlem8N  37128  ltrnnid  37287  sn-00id  39280  mptfcl  39366  fphpd  39462  elmnc  39785  itgoval  39810  arearect  39871  clsk3nimkb  40439  grumnud  40671  nanorxor  40686  pm11.71  40778  iotavalsb  40814  sbiota1  40815  2uasbanh  40944  eel0TT  41087  eelT00  41088  eelTTT  41089  eelT11  41090  eelT12  41092  eelTT1  41093  eelT01  41094  eel0T1  41095  eelTT  41154  uunT1p1  41164  uun121  41166  uun121p1  41167  un2122  41173  uunTT1  41176  uunTT1p1  41177  uunTT1p2  41178  uunT11  41179  uunT11p1  41180  uunT11p2  41181  uunT12  41182  uunT12p1  41183  uunT12p2  41184  uunT12p3  41185  uunT12p4  41186  uunT12p5  41187  uun111  41188  3anidm12p2  41190  uun123  41191  3impdirp1  41199  undif3VD  41265  ax6e2ndeqVD  41292  2uasbanhVD  41294  ax6e2ndeqALT  41314  iunconnlem2  41318  sineq0ALT  41320  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweidlem3  42337  stoweidlem17  42351  fourierdlem42  42483  fourierdlem48  42488  fourierdlem50  42490  fourierdlem51  42491  fourierdlem76  42516  fourierdlem83  42523  fourierdlem87  42527  hoidmvval0  42918  rexrsb  43347  2reu8i  43361  2reuimp  43363  afv0nbfvbi  43399  afvfv0bi  43400  afveu  43401  fnbrafvb  43402  afvres  43420  tz6.12-afv  43421  dmfcoafv  43423  afvco2  43424  aovprc  43436  aovrcl  43437  aovmpt4g  43449  afv2eu  43486  afv2res  43487  tz6.12-afv2  43488  tz6.12i-afv2  43491  afv2rnfveq  43510  fvmptrab  43540  fvmptrabdm  43541  fzopred  43571  2ffzoeq  43577  ichan  43679  elsprel  43686  prproropf1o  43718  reupr  43733  lighneal  43825  odd2prm2  43932  even3prm2  43933  upgrwlkupwlk  44064  ovn0ssdmfun  44083  islinindfis  44553  rrx2linest  44778  line2ylem  44787  setrec2fun  44844  elsetrecslem  44850  setrecsres  44853  secval  44895  cscval  44896  cotval  44897