MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbir Structured version   Visualization version   GIF version

Theorem sylbir 225
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
StepHypRef Expression
1 sylbir.1 . . 3 (𝜓𝜑)
21biimpri 218 . 2 (𝜑𝜓)
3 sylbir.2 . 2 (𝜓𝜒)
42, 3syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3imtr3i  280  ex  449  3ori  1428  19.38  1806  19.35  1845  equsex  2328  nfeqf2  2333  sbi2  2421  mo2v  2505  2mo  2580  axie2  2626  necon1bi  2851  necon1i  2856  sbhypf  3284  vtocl2  3292  vtocl3  3293  reu6  3428  uneqin  3911  difin0ss  3979  inelcm  4065  falseral0  4114  difprsn1  4362  tppreqb  4368  n0snor2el  4396  unissint  4533  intminss  4535  iununi  4642  bm1.3ii  4817  eusv2nf  4894  reusv3i  4905  reuxfr2d  4921  moabex  4957  copsex2g  4987  opelopabt  5016  eqrelrel  5255  opeliunxp2  5293  opelrn  5389  issref  5544  ssxpb  5603  xpima  5611  xpimasn  5614  dmsn0el  5639  relcoi2  5701  elsnxp  5715  elsnxpOLD  5716  iotanul  5904  dffv2  6310  fnfvrnss  6430  fressnfv  6467  fconst5  6512  f1mpt  6558  isocnv3  6622  f1owe  6643  ovprc  6723  onminesb  7040  onminsb  7041  onintrab  7043  onnminsb  7046  onsucuni2  7076  tfindsg2  7103  zfrep6  7176  fo1stres  7236  fo2ndres  7237  bropopvvv  7300  bropfvvvv  7302  frxp  7332  opeliunxp2f  7381  mpt2xopoveqd  7392  reldmtpos  7405  wfrlem4  7463  wfrlem12  7471  wfrlem16  7475  wfr2  7479  tfrlem5  7521  tfrlem9  7526  tfr2  7539  rdgsuc  7565  oaordi  7671  oeordi  7712  omopthi  7782  fvmptmap  7936  mptelixpg  7987  ener  8044  domtr  8050  snfi  8079  unen  8081  xpf1o  8163  mapen  8165  unxpdomlem3  8207  isinf  8214  frfi  8246  unblem1  8253  unfi  8268  fofinf1o  8282  fsuppun  8335  inf3lem2  8564  inf3lem5  8567  cantnfp1lem1  8613  cantnfp1lem3  8615  tcmin  8655  r1ordg  8679  r1ord  8681  rankr1ai  8699  r1val3  8739  bndrank  8742  unbndrank  8743  rankr1b  8765  rankxplim3  8782  tcrank  8785  xpnum  8815  cardmin2  8862  infxpenlem  8874  fseqen  8888  dfac8clem  8893  alephsson  8961  alephfp  8969  dfac4  8983  kmlem6  9015  kmlem8  9017  kmlem9  9018  infpssr  9168  fin1a2lem12  9271  axcc4  9299  axcc4dom  9301  ac6s2  9346  zornn0g  9365  cardidg  9408  unsnen  9413  pwcfsdom  9443  cfpwsdom  9444  gchpwdom  9530  r1tskina  9642  intgru  9674  indpi  9767  nqereu  9789  supsrlem  9970  letrii  10200  dfnn3  11072  zaddcl  11455  nn0ind  11510  fnn0ind  11514  ublbneg  11811  nn01to3  11819  infmrp1  12212  fz0  12394  fzo1fzo0n0  12558  elfzom1elp1fzo  12574  fzo0end  12600  elfznelfzo  12613  fzind2  12626  injresinjlem  12628  fleqceilz  12693  nnsinds  12827  nn0sinds  12828  faclbnd4lem1  13120  hashinf  13162  hasheqf1oi  13180  hashgt0elex  13227  hashfacen  13276  hash2prde  13290  hash2sspr  13308  fun2dmnop0  13314  swrdn0  13476  swrdlsw  13498  swrdswrdlem  13505  swrdccatin12lem3  13536  swrdccat3  13538  swrdccat3blem  13541  cshwsublen  13588  cshwidxmod  13595  repswcshw  13604  cshw1  13614  trclun  13799  dmtrclfv  13803  rediv  13915  imdiv  13922  sqrt0  14026  fsump1i  14544  modfsummods  14569  bpolydiflem  14829  bpoly3  14833  bpoly4  14834  cos1bnd  14961  sinltx  14963  rpnnen2lem1  14987  rpnnen2lem2  14988  rpnnen2lem12  14998  odd2np1  15112  opoe  15134  omoe  15135  opeo  15136  omeo  15137  gcdcllem1  15268  gcdaddmlem  15292  dfgcd2  15310  algfx  15340  lcmledvds  15359  lcmfunsnlem  15401  lcmfun  15405  coprmprod  15422  coprmproddvdslem  15423  prmn2uzge3OLD  15460  odzval  15543  odzdvds  15547  prmreclem5  15671  mul4sq  15705  prmgaplem5  15806  prmgaplem6  15807  imasaddfnlem  16235  mreexexlem4d  16354  joindmss  17054  meetdmss  17068  gictr  17764  cntzval  17800  symg2bas  17864  efgsfo  18198  efgrelexlemb  18209  dprddomcld  18446  dprdsubg  18469  dprd2da  18487  lssacs  19015  cnfldinv  19825  ocvval  20059  dmatmul  20351  mdetfval1  20444  mndifsplit  20490  fvmptnn04if  20702  opnnei  20972  ordtbas2  21043  ordtrest2lem  21055  lmmo  21232  fincmp  21244  bwth  21261  txbas  21418  ptcnplem  21472  tx2ndc  21502  hmphtr  21634  fbun  21691  filconn  21734  ptcmplem5  21907  cnextcn  21918  utoptop  22085  ucncn  22136  metust  22410  cfilucfil  22411  elcncf1di  22745  xrhmeo  22792  phtpycc  22837  copco  22864  pcohtpylem  22865  pcopt  22868  pcopt2  22869  ncvsi  22997  ovolval  23288  iunmbl2  23371  itg2splitlem  23560  cpnfval  23740  plyval  23994  fta1  24108  aaliou2b  24141  tayl0  24161  ulmdvlem3  24201  radcnvlem2  24213  dvradcnv  24220  reeff1o  24246  sincosq1lem  24294  sincosq2sgn  24296  sincosq4sgn  24298  sinq12ge0  24305  logrncl  24359  eflog  24368  cxpge0  24474  logb1  24552  atanf  24652  atanbnd  24698  igamf  24822  igamcl  24823  lgsne0  25105  mul2sq  25189  pntibnd  25327  ostth  25373  mptelee  25820  axlowdimlem9  25875  axlowdimlem12  25878  axcontlem2  25890  axcontlem12  25900  structgrssvtx  25958  structgrssiedg  25959  structgrssvtxOLD  25961  structgrssiedgOLD  25962  lpvtx  26008  nbuhgr  26284  nbumgr  26288  nbuhgr2vtx1edgblem  26292  nbgr0vtxlem  26296  nbgr1vtx  26299  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  prcliscplgr  26365  cusgrsizeinds  26404  sizusglecusglem2  26414  uhgrvd00  26486  fusgrregdegfi  26521  rusgr1vtxlem  26539  wlkeq  26585  wlk1walk  26591  uspgr2wlkeq  26598  wlklenvclwlk  26607  wlkreslem  26622  wlkdlem2  26636  wlkdlem4  26638  spthonepeq  26704  clwwisshclwws  26972  clwwlkneq0  26990  3wlkdlem6  27143  eupth2eucrct  27195  eupth2lem1  27196  eupth2lem3lem7  27212  frgr3vlem1  27253  frgr3vlem2  27254  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  numclwwlk5  27375  frgrreg  27381  frgrregord013  27382  friendshipgt3  27385  isgrpo  27479  vciOLD  27544  vcex  27561  nmogtmnf  27753  siilem1  27834  siii  27836  ajmoi  27842  bcsiALT  28164  hhcms  28188  ocval  28267  hsupval  28321  omlsilem  28389  h1de2bi  28541  h1de2ctlem  28542  hosubeq0i  28813  adjmo  28819  nmopgtmnf  28855  nlfnval  28868  nmcopex  29016  nmcfnex  29040  riesz4i  29050  riesz1  29052  riesz2  29053  opsqrlem1  29127  superpos  29341  hatomistici  29349  chpssati  29350  mdsymlem3  29392  3o1cs  29437  3o2cs  29438  3o3cs  29439  spc2ed  29440  brabgaf  29546  f1mptrn  29563  ffsrn  29632  fpwrelmap  29636  ordtrest2NEWlem  30096  qqhval2  30154  esumfsup  30260  esumcvg  30276  cntnevol  30419  ddemeas  30427  dya2icoseg2  30468  dya2iocnei  30472  eulerpartlems  30550  eulerpartlemgvv  30566  eulerpart  30572  cndprobprob  30628  ballotlemsdom  30701  ballotth  30727  sgn3da  30731  bnj945  30970  bnj1379  31027  bnj1459  31039  bnj557  31097  bnj571  31102  bnj849  31121  bnj964  31139  bnj978  31145  bnj1018  31158  bnj1020  31159  bnj1033  31163  bnj1175  31198  bnj1398  31228  bnj1417  31235  bnj1523  31265  txpconn  31340  msubco  31554  mclsax  31592  setinds  31807  dfon2lem7  31818  dfon2lem8  31819  poseq  31878  soseq  31879  frrlem4  31908  nocvxminlem  32018  nocvxmin  32019  pprodss4v  32116  fullfunfv  32179  altxpsspw  32209  funtransport  32263  fvtransport  32264  funray  32372  fvray  32373  funline  32374  fvline  32376  finminlem  32437  bisym1  32543  onsucconni  32561  onsucsuccmpi  32567  bj-alcomexcom  32795  axc11n11r  32798  bj-equsal2  32937  bj-xpima1snALT  33069  mptsnunlem  33315  iooelexlt  33340  relowlpssretop  33342  rdgeqoa  33348  wl-dveeq12  33441  wl-lem-nexmo  33479  matunitlindflem1  33535  ptrecube  33539  poimirlem26  33565  poimirlem30  33569  poimir  33572  ismblfin  33580  itg2addnclem  33591  dvasin  33626  sdclem2  33668  totbndbnd  33718  ismgmOLD  33779  exidresid  33808  isrngo  33826  rngoablo2  33838  rngoueqz  33869  isdivrngo  33879  isdrngo1  33885  isdrngo2  33887  ispridl2  33967  relcnveq3  34233  elrelscnveq3  34381  prtlem11  34470  ax12eq  34545  ax12el  34546  lkr0f  34699  hl2at  35009  dalemswapyz  35260  pclfinclN  35554  osumcllem11N  35570  pexmidlem8N  35581  ltrnnid  35740  mptfcl  37600  fphpd  37697  elmnc  38023  itgoval  38048  arearect  38118  clsk3nimkb  38655  nanorxor  38821  pm11.71  38914  iotavalsb  38951  sbiota1  38952  2uasbanh  39094  eel0TT  39246  eelT00  39247  eelTTT  39248  eelT11  39249  eelT12  39251  eelTT1  39252  eelT01  39253  eel0T1  39254  eelTT  39315  uunT1p1  39325  uun121  39327  uun121p1  39328  un2122  39334  uunTT1  39337  uunTT1p1  39338  uunTT1p2  39339  uunT11  39340  uunT11p1  39341  uunT11p2  39342  uunT12  39343  uunT12p1  39344  uunT12p2  39345  uunT12p3  39346  uunT12p4  39347  uunT12p5  39348  uun111  39349  3anidm12p2  39351  uun123  39352  3impdirp1  39360  undif3VD  39432  ax6e2ndeqVD  39459  2uasbanhVD  39461  ax6e2ndeqALT  39481  iunconnlem2  39485  sineq0ALT  39487  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem3  40538  stoweidlem17  40552  fourierdlem42  40684  fourierdlem48  40689  fourierdlem50  40691  fourierdlem51  40692  fourierdlem76  40717  fourierdlem83  40724  fourierdlem87  40728  hoidmvval0  41122  rexrsb  41490  raaan2  41496  afv0nbfvbi  41552  afvfv0bi  41553  afveu  41554  fnbrafvb  41555  afvres  41573  tz6.12-afv  41574  dmfcoafv  41576  afvco2  41577  aovprc  41589  aovrcl  41590  aovmpt4g  41602  fvmptrab  41631  fvmptrabdm  41632  fzopred  41657  2ffzoeq  41663  pfxccat3  41751  pfxccat3a  41754  lighneal  41853  odd2prm2  41952  even3prm2  41953  upgrwlkupwlk  42046  elsprel  42050  ovn0ssdmfun  42092  islinindfis  42563  setrec2fun  42764  elsetrecslem  42770  setrecsres  42773  secval  42816  cscval  42817  cotval  42818
  Copyright terms: Public domain W3C validator