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

Theorem sylbir 223
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 216 . 2 (𝜑𝜓)
3 sylbir.2 . 2 (𝜓𝜒)
42, 3syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3imtr3i  278  ex  448  3ori  1379  19.38  1756  19.35  1793  equsex  2280  nfeqf2  2284  sbi2  2380  mo2v  2464  2mo  2538  axie2  2584  necon1bi  2809  necon1i  2814  sbhypf  3225  vtocl2  3233  vtocl3  3234  reu6  3361  uneqin  3836  difin0ss  3899  inelcm  3983  difprsn1  4270  tppreqb  4276  unissint  4430  intminss  4432  iununi  4540  bm1.3ii  4706  eusv2nf  4784  reusv3i  4795  reuxfr2d  4811  moabex  4847  copsex2g  4877  opelopabt  4901  eqrelrel  5132  opeliunxp2  5169  opelrn  5264  issref  5414  ssxpb  5472  xpima  5480  xpimasn  5483  dmsn0el  5507  relcoi2  5565  elsnxp  5579  elsnxpOLD  5580  iotanul  5768  dffv2  6165  fnfvrnss  6281  fressnfv  6309  fconst5  6353  f1mpt  6396  isocnv3  6459  f1owe  6480  ovprc  6558  onminesb  6867  onminsb  6868  onintrab  6870  onnminsb  6873  onsucuni2  6903  tfindsg2  6930  zfrep6  7004  fo1stres  7060  fo2ndres  7061  bropopvvv  7119  bropfvvvv  7121  frxp  7151  opeliunxp2f  7200  mpt2xopoveqd  7211  reldmtpos  7224  wfrlem4  7282  wfrlem12  7290  wfrlem16  7294  wfr2  7298  tfrlem5  7340  tfrlem9  7345  tfr2  7358  rdgsuc  7384  oaordi  7490  oeordi  7531  omopthi  7601  fvmptmap  7757  mptelixpg  7808  ener  7865  enerOLD  7866  domtr  7872  snfi  7900  unen  7902  xpf1o  7984  mapen  7986  unxpdomlem3  8028  isinf  8035  frfi  8067  unblem1  8074  unfi  8089  fofinf1o  8103  fsuppun  8154  inf3lem2  8386  inf3lem5  8389  cantnfp1lem1  8435  cantnfp1lem3  8437  tcmin  8477  r1ordg  8501  r1ord  8503  rankr1ai  8521  r1val3  8561  bndrank  8564  unbndrank  8565  rankr1b  8587  rankxplim3  8604  tcrank  8607  xpnum  8637  cardmin2  8684  infxpenlem  8696  fseqen  8710  dfac8clem  8715  alephsson  8783  alephfp  8791  dfac4  8805  kmlem6  8837  kmlem8  8839  kmlem9  8840  infpssr  8990  fin1a2lem12  9093  axcc4  9121  axcc4dom  9123  ac6s2  9168  zornn0g  9187  cardidg  9226  unsnen  9231  pwcfsdom  9261  cfpwsdom  9262  gchpwdom  9348  r1tskina  9460  intgru  9492  indpi  9585  nqereu  9607  supsrlem  9788  letrii  10013  dfnn3  10883  zaddcl  11252  nn0ind  11306  fnn0ind  11310  ublbneg  11607  nn01to3  11615  infmrp1  12003  fz0  12184  fzo1fzo0n0  12343  elfzom1elp1fzo  12359  fzo0end  12383  elfznelfzo  12396  fzind2  12405  injresinjlem  12407  fleqceilz  12472  nnsinds  12606  nn0sinds  12607  faclbnd4lem1  12899  hashinf  12941  hasheqf1oi  12956  hasheqf1oiOLD  12957  hashgt0elex  13004  hashfacen  13049  hash2prde  13063  hash2sspr  13076  swrdn0  13230  swrdlsw  13252  swrdswrdlem  13259  swrdccatin12lem3  13289  swrdccat3  13291  swrdccat3blem  13294  cshwsublen  13341  cshwidxmod  13348  repswcshw  13357  cshw1  13367  trclun  13551  dmtrclfv  13555  rediv  13667  imdiv  13674  sqrt0  13778  fsump1i  14290  modfsummods  14314  bpolydiflem  14572  bpoly3  14576  bpoly4  14577  cos1bnd  14704  sinltx  14706  rpnnen2lem1  14730  rpnnen2lem2  14731  rpnnen2lem12  14741  odd2np1  14851  opoe  14873  omoe  14874  opeo  14875  omeo  14876  gcdcllem1  15007  gcdaddmlem  15031  dfgcd2  15049  algfx  15079  lcmledvds  15098  lcmfunsnlem  15140  lcmfun  15144  coprmprod  15161  coprmproddvdslem  15162  prmn2uzge3OLD  15199  odzval  15282  odzdvds  15286  prmreclem5  15410  mul4sq  15444  prmgaplem5  15545  prmgaplem6  15546  imasaddfnlem  15959  mreexexlem4d  16078  joindmss  16778  meetdmss  16792  gictr  17488  cntzval  17525  symg2bas  17589  efgsfo  17923  efgrelexlemb  17934  dprddomcld  18171  dprdsubg  18194  dprd2da  18212  lssacs  18736  cnfldinv  19544  ocvval  19777  dmatmul  20069  mdetfval1  20162  mndifsplit  20208  fvmptnn04if  20420  opnnei  20681  ordtbas2  20752  ordtrest2lem  20764  lmmo  20941  fincmp  20953  bwth  20970  txbas  21127  ptcnplem  21181  tx2ndc  21211  hmphtr  21343  fbun  21401  filcon  21444  ptcmplem5  21617  cnextcn  21628  utoptop  21795  ucncn  21846  metust  22120  cfilucfil  22121  elcncf1di  22453  xrhmeo  22500  phtpycc  22545  copco  22573  pcohtpylem  22574  pcopt  22577  pcopt2  22578  ncvsi  22703  ovolval  22993  iunmbl2  23076  itg2splitlem  23265  cpnfval  23445  plyval  23697  fta1  23811  aaliou2b  23844  ulmdvlem3  23904  radcnvlem2  23916  dvradcnv  23923  reeff1o  23949  sincosq1lem  23997  sincosq2sgn  23999  sincosq4sgn  24001  sinq12ge0  24008  logrncl  24062  eflog  24071  cxpge0  24173  logb1  24251  atanf  24351  atanbnd  24397  igamf  24521  igamcl  24522  lgsne0  24804  mul2sq  24888  pntibnd  25026  ostth  25072  mptelee  25520  axlowdimlem9  25575  axlowdimlem12  25578  axcontlem2  25590  axcontlem12  25600  isusgra0  25669  usgraop  25672  usgraedg4  25709  nbusgra  25750  nbgranself2  25758  wlkn0  25848  wlkcpr  25850  wlkntrllem3  25884  spthonepeq  25910  wlkdvspth  25931  cyclnspth  25952  3v3e3cycl2  25985  3v3e3cycl  25986  4cycl4dv  25988  2wlkeq  26028  usg2wlkeq  26029  clwwlknprop  26093  clwwisshclww  26128  wlklenvclwlk  26159  2wlkonot3v  26195  2spthonot3v  26196  2spontn0vne  26207  vdgrf  26218  usgfiregdegfi  26231  nbhashuvtx1  26235  eupath2lem1  26297  frgra3vlem1  26320  frgra3vlem2  26321  frgrancvvdeqlem2  26351  frgrancvvdeqlem3  26352  frgrancvvdeqlemB  26358  frgrancvvdeqlemC  26359  frgrawopreglem5  26368  usgreghash2spot  26389  numclwwlk5  26432  frgrareg  26437  frgraregord013  26438  friendshipgt3  26441  isgrpo  26528  vciOLD  26593  vcex  26610  nmogtmnf  26802  siilem1  26883  siii  26885  ajmoi  26891  bcsiALT  27213  hhcms  27237  ocval  27316  hsupval  27370  omlsilem  27438  h1de2bi  27590  h1de2ctlem  27591  hosubeq0i  27862  adjmo  27868  nmopgtmnf  27904  nlfnval  27917  nmcopex  28065  nmcfnex  28089  riesz4i  28099  riesz1  28101  riesz2  28102  opsqrlem1  28176  superpos  28390  hatomistici  28398  chpssati  28399  mdsymlem3  28441  3o1cs  28486  3o2cs  28487  3o3cs  28488  spc2ed  28489  brabgaf  28593  f1mptrn  28609  ffsrn  28685  fpwrelmap  28689  ordtrest2NEWlem  29089  qqhval2  29147  esumfsup  29252  esumcvg  29268  cntnevol  29411  ddemeas  29419  dya2icoseg2  29460  dya2iocnei  29464  eulerpartlems  29542  eulerpartlemgvv  29558  eulerpart  29564  cndprobprob  29620  ballotlemsdom  29693  ballotth  29719  sgn3da  29723  bnj945  29891  bnj1379  29948  bnj1459  29960  bnj557  30018  bnj571  30023  bnj849  30042  bnj964  30060  bnj978  30066  bnj1018  30079  bnj1020  30080  bnj1033  30084  bnj1175  30119  bnj1398  30149  bnj1417  30156  bnj1523  30186  txpcon  30261  msubco  30475  mclsax  30513  setinds  30720  dfon2lem7  30731  dfon2lem8  30732  poseq  30787  soseq  30788  frrlem4  30820  frrlem11  30829  nodenselem4  30876  nocvxminlem  30882  nocvxmin  30883  pprodss4v  30954  fullfunfv  31017  altxpsspw  31047  funtransport  31101  fvtransport  31102  funray  31210  fvray  31211  funline  31212  fvline  31214  finminlem  31275  bisym1  31381  onsucconi  31399  onsucsuccmpi  31405  bj-alcomexcom  31650  axc11n11r  31653  bj-equsal2  31793  bj-xpima1snALT  31920  mptsnunlem  32144  iooelexlt  32169  relowlpssretop  32171  rdgeqoa  32177  wl-dveeq12  32273  wl-lem-nexmo  32311  matunitlindflem1  32358  ptrecube  32362  poimirlem26  32388  poimirlem30  32392  poimir  32395  ismblfin  32403  itg2addnclem  32414  dvasin  32449  sdclem2  32491  totbndbnd  32541  ismgmOLD  32602  exidresid  32631  isrngo  32649  rngoablo2  32661  rngoueqz  32692  isdivrngo  32702  isdrngo1  32708  isdrngo2  32710  ispridl2  32790  prtlem11  32952  ax12eq  33027  ax12el  33028  lkr0f  33182  hl2at  33492  dalemswapyz  33743  pclfinclN  34037  osumcllem11N  34053  pexmidlem8N  34064  ltrnnid  34223  mptfcl  36084  fphpd  36181  elmnc  36508  itgoval  36533  arearect  36603  clsk3nimkb  37141  nanorxor  37309  pm11.71  37402  iotavalsb  37439  sbiota1  37440  2uasbanh  37581  eel0TT  37733  eelT00  37734  eelTTT  37735  eelT11  37736  eelT12  37738  eelTT1  37739  eelT01  37740  eel0T1  37741  eelTT  37802  uunT1p1  37812  uun121  37814  uun121p1  37815  un2122  37821  uunTT1  37824  uunTT1p1  37825  uunTT1p2  37826  uunT11  37827  uunT11p1  37828  uunT11p2  37829  uunT12  37830  uunT12p1  37831  uunT12p2  37832  uunT12p3  37833  uunT12p4  37834  uunT12p5  37835  uun111  37836  3anidm12p2  37838  uun123  37839  3impdirp1  37847  undif3VD  37923  ax6e2ndeqVD  37950  2uasbanhVD  37952  ax6e2ndeqALT  37972  iunconlem2  37976  sineq0ALT  37978  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  stoweidlem3  38679  stoweidlem17  38693  fourierdlem42  38825  fourierdlem48  38830  fourierdlem50  38832  fourierdlem51  38833  fourierdlem76  38858  fourierdlem83  38865  fourierdlem87  38869  hoidmvval0  39260  rexrsb  39601  raaan2  39607  afv0nbfvbi  39664  afvfv0bi  39665  afveu  39666  fnbrafvb  39667  afvres  39685  tz6.12-afv  39686  dmfcoafv  39688  afvco2  39689  aovprc  39701  aovrcl  39702  aovmpt4g  39714  fzopred  39729  lighneal  39850  pfxccat3  40073  pfxccat3a  40076  falseral0  40092  n0snor2el  40102  fun2dmnop0  40133  2ffzoeq  40167  structgrssvtx  40238  structgrssiedg  40239  lpvtx  40271  nbuhgr  40546  nbumgr  40550  nbuhgr2vtx1edgblem  40554  nbgr0vtxlem  40558  nbgr1vtx  40561  uvtxa01vtx0  40604  cusgrsizeinds  40649  sizusglecusglem2  40659  uhgrvd00  40731  fusgrregdegfi  40750  rusgr1vtxlem  40768  1wlkeq  40819  1wlk1walk  40824  upgr1wlkwlk  40828  uspgr2wlkeq  40835  1wlklenvclwlk  40844  1wlkreslem  40859  1wlkdlem2  40873  1wlkdlem4  40875  spthonepeq-av  40939  clwwisshclwws  41216  31wlkdlem6  41313  eupth2eucrct  41366  eupth2lem1  41367  eupth2lem3lem7  41383  frgr3vlem1  41424  frgr3vlem2  41425  frgrncvvdeqlem2  41451  frgrncvvdeqlem3  41452  frgrncvvdeqlemB  41458  frgrncvvdeqlemC  41459  frgrwopreglem5  41466  fusgreghash2wsp  41483  av-numclwwlk5  41523  av-frgrareg  41529  av-frgraregord013  41530  av-friendshipgt3  41533  ovn0ssdmfun  41538  islinindfis  42013  secval  42229  cscval  42230  cotval  42231
  Copyright terms: Public domain W3C validator