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

Theorem sylbir 213
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbir.1  |-  ( ps  <->  ph )
sylbir.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
sylbir  |-  ( ph  ->  ch )

Proof of Theorem sylbir
StepHypRef Expression
1 sylbir.1 . . 3  |-  ( ps  <->  ph )
21biimpri 206 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr3i  265  ex  434  3ori  1271  19.38  1629  equsex  1985  nfeqf2  1988  sbi2  2083  sb5rfOLD  2123  ax12eq  2243  ax12el  2244  mo2v  2260  moOLD  2300  mo2OLD  2309  2mo  2355  2moOLD  2356  axie2  2409  bm1.1  2418  necon1i  2645  sbhypf  3008  vtocl2  3014  vtocl3  3015  reu6  3137  uneqin  3589  inelcm  3721  difin0ss  3733  difprsn1  3998  tppreqb  4002  unissint  4140  intminss  4142  iununi  4243  bm1.3ii  4404  eusv2nf  4478  reusv3i  4487  reuxfr2d  4503  moabex  4539  copsex2g  4567  opelopabt  4590  eqrelrel  4928  opeliunxp2  4965  opelrn  5058  issref  5199  ssxpb  5260  xpima  5268  xpimasn  5271  dmsn0el  5296  relcoi2  5353  iotanul  5384  dffv2  5752  fnfvrnss  5858  fressnfv  5883  fconst5  5922  fconstfv  5927  f1mpt  5961  isocnv3  6010  f1owe  6031  ovprc  6107  onminesb  6398  onminsb  6399  onintrab  6401  onnminsb  6404  onsucuni2  6434  tfindsg2  6461  zfrep6  6534  fo1stres  6589  fo2ndres  6590  bropopvvv  6642  frxp  6671  mpt2xopoveqd  6727  reldmtpos  6742  tfrlem5  6825  tfrlem9  6830  tfr2  6843  rdgsuc  6866  oaordi  6973  oeordi  7014  omopthi  7084  fvmptmap  7237  mptelixpg  7288  ener  7344  domtr  7350  snfi  7378  unen  7380  xpf1o  7461  mapen  7463  unxpdomlem3  7507  isinf  7514  frfi  7545  unblem1  7552  unfi  7567  fofinf1o  7580  fsuppun  7627  inf3lem2  7823  inf3lem5  7826  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  tcmin  7949  r1ordg  7973  r1ord  7975  rankr1ai  7993  r1val3  8033  bndrank  8036  unbndrank  8037  rankr1b  8059  rankxplim3  8076  tcrank  8079  xpnum  8109  cardmin2  8156  infxpenlem  8168  fseqen  8185  dfac8clem  8190  alephsson  8258  alephfp  8266  dfac4  8280  kmlem6  8312  kmlem8  8314  kmlem9  8315  infpssr  8465  fin1a2lem12  8568  axcc4  8596  axcc4dom  8598  ac6s2  8643  zornn0g  8662  cardidg  8700  unsnen  8705  pwcfsdom  8735  cfpwsdom  8736  gchpwdom  8824  r1tskina  8936  intgru  8968  indpi  9063  nqereu  9085  supsrlem  9265  letrii  9486  infmrcl  10296  dfnn3  10323  zaddcl  10672  uzindOLD  10723  nn0ind  10725  fnn0ind  10728  ublbneg  10926  fz0  11451  fzo1fzo0n0  11571  fzo0end  11602  elfznelfzo  11613  fzind2  11620  injresinjlem  11621  fleqceilz  11676  faclbnd4lem1  12052  hashinf  12091  hasheqf1oi  12105  hashgt0elex  12142  hash2prde  12162  hashfacen  12190  lswcl  12253  swrdlsw  12329  swrdswrdlem  12336  swrdccatin12lem3  12364  swrdccat3  12366  swrdccat3blem  12369  cshwsublen  12416  cshwidxmod  12423  repswcshw  12429  cshw1  12439  rediv  12603  imdiv  12610  sqr0  12714  fsump1i  13219  cos1bnd  13453  sinltx  13455  rpnnen2lem1  13479  rpnnen2lem2  13480  rpnnen2  13490  odd2np1  13574  gcdcllem1  13677  gcdaddmlem  13694  algfx  13737  odzval  13845  odzdvds  13849  opoe  13860  omoe  13861  opeo  13862  omeo  13863  prmreclem5  13963  mul4sq  13997  imasaddfnlem  14448  mreexexlem4d  14567  joindmss  15159  meetdmss  15173  gictr  15782  cntzval  15818  symg2bas  15882  efgsfo  16215  efgrelexlemb  16226  dprddomcld  16456  dprdsubg  16494  dprd2da  16514  lssacs  16969  cnfldinv  17690  ocvval  17933  mdetfval1  18242  mndifsplit  18283  eltopspOLD  18364  tpsexOLD  18365  opnnei  18565  ordtbas2  18636  ordtrest2lem  18648  lmmo  18825  fincmp  18837  bwth  18854  txbas  18981  ptcnplem  19035  tx2ndc  19065  hmphtr  19197  fbun  19254  filcon  19297  ptcmplem5  19469  cnextcn  19480  utoptop  19650  restutopopn  19654  ucncn  19701  metustOLD  19983  metust  19984  cfilucfilOLD  19985  cfilucfil  19986  elcncf1di  20312  xrhmeo  20359  phtpycc  20404  copco  20431  pcohtpylem  20432  pcopt  20435  pcopt2  20436  ovolval  20798  iunmbl2  20879  itg2splitlem  21067  cpnfval  21247  plyval  21545  fta1  21658  aaliou2b  21691  ulmdvlem3  21751  radcnvlem2  21763  dvradcnv  21770  reeff1o  21796  sincosq1lem  21843  sincosq2sgn  21845  sincosq4sgn  21847  sinq12ge0  21854  logrncl  21903  eflog  21912  cxpge0  22012  atanf  22159  atanbnd  22205  lgsne0  22556  mul2sq  22588  pntibnd  22726  ostth  22772  mptelee  22963  axlowdimlem9  23018  axlowdimlem12  23021  axcontlem2  23033  axcontlem12  23043  isusgra0  23097  usgraedg4  23127  nbusgra  23161  nbgranself2  23169  wlkntrllem3  23282  spthonepeq  23308  wlkdvspth  23329  cyclnspth  23339  3v3e3cycl2  23372  3v3e3cycl  23373  4cycl4dv  23375  vdgrf  23390  eupath2lem1  23420  isgrpo  23505  ismgm  23629  isrngo  23687  rngoablo2  23731  rngoueqz  23739  isdivrngo  23740  vci  23748  vcex  23780  nmogtmnf  23992  siilem1  24073  siii  24075  ajmoi  24081  bcsiALT  24403  hhcms  24427  ocval  24505  hsupval  24559  omlsilem  24627  h1de2bi  24779  h1de2ctlem  24780  hosubeq0i  25052  adjmo  25058  nmopgtmnf  25094  nlfnval  25107  nmcopex  25255  nmcfnex  25279  riesz4i  25289  riesz1  25291  riesz2  25292  opsqrlem1  25366  superpos  25580  hatomistici  25588  chpssati  25589  mdsymlem3  25631  mdsymi  25637  3o1cs  25676  3o2cs  25677  3o3cs  25678  ffsrn  25853  fpwrelmap  25857  ordtrest2NEWlem  26205  qqhval2  26264  logb1  26315  esumfsup  26372  esumcvg  26388  cntnevol  26495  ddemeas  26505  dya2icoseg2  26546  dya2iocnei  26550  eulerpartlems  26590  eulerpartlemgvv  26606  eulerpart  26612  cndprobprob  26668  ballotlemsdom  26741  ballotth  26767  sgn3da  26771  igamf  26884  igamcl  26885  txpcon  26968  ghomgrp  27155  setinds  27437  dfon2lem7  27448  dfon2lem8  27449  nnsinds  27524  nn0sinds  27525  poseq  27560  soseq  27561  wfrlem4  27573  wfrlem12  27581  wfrlem16  27585  wfr2  27587  frrlem4  27617  frrlem11  27626  nodenselem4  27671  nocvxminlem  27677  nocvxmin  27678  pprodss4v  27761  fullfunfv  27824  altxpsspw  27854  funtransport  27908  fvtransport  27909  funray  28017  fvray  28018  funline  28019  fvline  28021  bpolydiflem  28043  bpoly3  28047  bpoly4  28048  bisym1  28112  onsucconi  28130  onsucsuccmpi  28136  ismblfin  28273  itg2addnclem  28284  dvasin  28321  finminlem  28354  sdclem2  28479  totbndbnd  28529  exidresid  28585  isdrngo1  28603  isdrngo2  28605  ispridl2  28679  prtlem11  28853  mptfcl  28898  fphpd  28997  elmnc  29335  itgoval  29360  arearect  29433  pm11.71  29492  iotavalsb  29529  sbiota1  29530  stoweidlem3  29641  stoweidlem17  29655  rexrsb  29836  raaan2  29842  afv0nbfvbi  29900  afvfv0bi  29901  afveu  29902  fnbrafvb  29903  afvres  29921  tz6.12-afv  29922  dmfcoafv  29924  afvco2  29925  aovprc  29937  aovrcl  29938  aovmpt4g  29950  nn01to3  30030  2ffzoeq  30057  modfsummods  30087  lswccats1fst  30105  wlkn0  30122  2wlkeq  30131  usg2wlkeq  30132  wlkcpr  30133  2wlkonot3v  30237  2spthonot3v  30238  2spontn0vne  30249  clwwlknprop  30278  clwwisshclww  30314  wlkp1lenfislenp  30355  usgfiregdegfi  30371  nbhashuvtx1  30376  frgra3vlem1  30435  frgra3vlem2  30436  frgrancvvdeqlem2  30467  frgrancvvdeqlem3  30468  frgrancvvdeqlemB  30474  frgrancvvdeqlemC  30475  frgrawopreglem5  30484  usgreghash2spot  30505  frgrareg  30553  frgraregord013  30554  friendshipgt3  30557  islinindfis  30689  secval  30788  cscval  30789  cotval  30790  2uasbanh  30968  eel0TT  31127  eelT00  31128  eelTTT  31129  eelT11  31131  eelT12  31135  eelTT1  31137  eelT01  31138  eel0T1  31139  eelTT  31203  uunT1p1  31213  uun121  31215  uun121p1  31216  un2122  31222  uunTT1  31225  uunTT1p1  31226  uunTT1p2  31227  uunT11  31228  uunT11p1  31229  uunT11p2  31230  uunT12  31231  uunT12p1  31232  uunT12p2  31233  uunT12p3  31234  uunT12p4  31235  uunT12p5  31236  uun111  31237  3anidm12p2  31239  uun123  31240  3impdirp1  31248  undif3VD  31317  ax6e2ndeqVD  31344  2uasbanhVD  31346  ax6e2ndeqALT  31366  iunconlem2  31370  sineq0ALT  31372  bnj945  31466  bnj1379  31523  bnj1459  31535  bnj557  31593  bnj571  31598  bnj849  31617  bnj964  31635  bnj978  31641  bnj1018  31654  bnj1020  31655  bnj1033  31659  bnj1175  31694  bnj1398  31724  bnj1417  31731  bnj1523  31761  bj-equsexv  31876  bj-equsal2  31950  bj-xpima1snALT  32029  lkr0f  32309  hl2at  32619  dalemswapyz  32870  pclfinclN  33164  osumcllem11N  33180  pexmidlem8N  33191  ltrnnid  33350
  Copyright terms: Public domain W3C validator