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

Theorem sylbir 216
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-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 209 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 17 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3imtr3i  268  ex  435  3ori  1324  19.38  1706  19.35  1734  equsex  2095  nfeqf2  2100  sbi2  2191  mo2v  2276  2mo  2350  axie2  2396  necon1bi  2653  necon1i  2662  sbhypf  3128  vtocl2  3134  vtocl3  3135  reu6  3259  uneqin  3724  inelcm  3849  difin0ss  3863  difprsn1  4136  tppreqb  4141  unissint  4280  intminss  4282  iununi  4387  bm1.3ii  4549  eusv2nf  4622  reusv3i  4631  reuxfr2d  4644  moabex  4680  copsex2g  4708  opelopabt  4732  eqrelrel  4955  opeliunxp2  4992  opelrn  5085  issref  5232  ssxpb  5290  xpima  5298  xpimasn  5301  dmsn0el  5324  relcoi2  5382  elsnxp  5397  iotanul  5580  dffv2  5954  fnfvrnss  6066  fressnfv  6093  fconst5  6137  fconstfvOLD  6142  f1mpt  6177  isocnv3  6238  f1owe  6259  ovprc  6335  onminesb  6639  onminsb  6640  onintrab  6642  onnminsb  6645  onsucuni2  6675  tfindsg2  6702  zfrep6  6775  fo1stres  6831  fo2ndres  6832  bropopvvv  6887  frxp  6917  opeliunxp2f  6967  mpt2xopoveqd  6978  reldmtpos  6992  wfrlem4  7050  wfrlem12  7058  wfrlem16  7062  wfr2  7066  tfrlem5  7109  tfrlem9  7114  tfr2  7127  rdgsuc  7153  oaordi  7258  oeordi  7299  omopthi  7369  fvmptmap  7519  mptelixpg  7570  ener  7626  domtr  7632  snfi  7660  unen  7662  xpf1o  7743  mapen  7745  unxpdomlem3  7787  isinf  7794  frfi  7825  unblem1  7832  unfi  7847  fofinf1o  7861  fsuppun  7911  inf3lem2  8143  inf3lem5  8146  cantnfp1lem1  8191  cantnfp1lem3  8193  tcmin  8233  r1ordg  8257  r1ord  8259  rankr1ai  8277  r1val3  8317  bndrank  8320  unbndrank  8321  rankr1b  8343  rankxplim3  8360  tcrank  8363  xpnum  8393  cardmin2  8440  infxpenlem  8452  fseqen  8465  dfac8clem  8470  alephsson  8538  alephfp  8546  dfac4  8560  kmlem6  8592  kmlem8  8594  kmlem9  8595  infpssr  8745  fin1a2lem12  8848  axcc4  8876  axcc4dom  8878  ac6s2  8923  zornn0g  8942  cardidg  8980  unsnen  8985  pwcfsdom  9015  cfpwsdom  9016  gchpwdom  9102  r1tskina  9214  intgru  9246  indpi  9339  nqereu  9361  supsrlem  9542  letrii  9766  infmrclOLD  10600  dfnn3  10630  zaddcl  10984  nn0ind  11037  fnn0ind  11041  ublbneg  11255  nn01to3  11264  infmrp1  11641  fz0  11821  fzo1fzo0n0  11964  elfzom1elp1fzo  11987  fzo0end  12009  elfznelfzo  12020  fzind2  12029  injresinjlem  12030  fleqceilz  12087  nnsinds  12206  nn0sinds  12207  fsuppmapnn0fiubex  12210  faclbnd4lem1  12484  hashinf  12526  hasheqf1oi  12540  hashgt0elex  12584  hashfacen  12621  hash2prde  12635  hash2sspr  12648  swrdn0  12788  swrdlsw  12810  swrdswrdlem  12817  swrdccatin12lem3  12848  swrdccat3  12850  swrdccat3blem  12853  cshwsublen  12900  cshwidxmod  12907  repswcshw  12913  cshw1  12923  trclun  13078  dmtrclfv  13082  rediv  13194  imdiv  13201  sqrt0  13305  fsump1i  13829  modfsummods  13852  bpolydiflem  14106  bpoly3  14110  bpoly4  14111  cos1bnd  14240  sinltx  14242  rpnnen2lem1  14266  rpnnen2lem2  14267  rpnnen2  14277  odd2np1  14364  gcdcllem1  14472  gcdaddmlem  14491  algfx  14538  lcmledvds  14563  lcmsledvdsOLD  14584  lcmfunsnlem  14613  lcmfun  14617  coprmprod  14677  coprmproddvdslem  14678  odzval  14735  odzdvds  14739  odzvalOLD  14741  odzdvdsOLD  14745  opoe  14760  omoe  14761  opeo  14762  omeo  14763  prmreclem5  14863  mul4sq  14897  prmgaplem5  15024  prmgaplem6  15025  imasaddfnlem  15433  mreexexlem4d  15552  joindmss  16252  meetdmss  16266  gictr  16938  cntzval  16974  symg2bas  17038  efgsfo  17388  efgrelexlemb  17399  dprddomcld  17632  dprdsubg  17656  dprd2da  17674  lssacs  18189  cnfldinv  18998  ocvval  19228  dmatmul  19520  mdetfval1  19613  mndifsplit  19659  fvmptnn04if  19871  opnnei  20134  ordtbas2  20205  ordtrest2lem  20217  lmmo  20394  fincmp  20406  bwth  20423  txbas  20580  ptcnplem  20634  tx2ndc  20664  hmphtr  20796  fbun  20853  filcon  20896  ptcmplem5  21069  cnextcn  21080  utoptop  21247  ucncn  21298  metust  21571  cfilucfil  21572  elcncf1di  21925  xrhmeo  21972  phtpycc  22020  copco  22047  pcohtpylem  22048  pcopt  22051  pcopt2  22052  ovolval  22424  ovolvalOLD  22425  iunmbl2  22508  itg2splitlem  22704  cpnfval  22884  plyval  23145  fta1  23259  aaliou2b  23295  ulmdvlem3  23355  radcnvlem2  23367  dvradcnv  23374  reeff1o  23400  sincosq1lem  23450  sincosq2sgn  23452  sincosq4sgn  23454  sinq12ge0  23461  logrncl  23515  eflog  23524  cxpge0  23626  logb1  23704  atanf  23804  atanbnd  23850  igamf  23974  igamcl  23975  lgsne0  24259  mul2sq  24291  pntibnd  24429  ostth  24475  mptelee  24923  axlowdimlem9  24978  axlowdimlem12  24981  axcontlem2  24993  axcontlem12  25003  isusgra0  25072  usgraop  25075  usgraedg4  25112  nbusgra  25154  nbgranself2  25162  wlkn0  25253  wlkcpr  25255  wlkntrllem3  25289  spthonepeq  25315  wlkdvspth  25336  cyclnspth  25357  3v3e3cycl2  25390  3v3e3cycl  25391  4cycl4dv  25393  2wlkeq  25433  usg2wlkeq  25434  clwwlknprop  25498  clwwisshclww  25533  wlklenvclwlk  25565  2wlkonot3v  25601  2spthonot3v  25602  2spontn0vne  25613  vdgrf  25624  usgfiregdegfi  25637  nbhashuvtx1  25641  eupath2lem1  25703  frgra3vlem1  25726  frgra3vlem2  25727  frgrancvvdeqlem2  25757  frgrancvvdeqlem3  25758  frgrancvvdeqlemB  25764  frgrancvvdeqlemC  25765  frgrawopreglem5  25774  usgreghash2spot  25795  frgrareg  25843  frgraregord013  25844  friendshipgt3  25847  isgrpo  25922  ismgmOLD  26046  isrngo  26104  rngoablo2  26148  rngoueqz  26156  isdivrngo  26157  vci  26165  vcex  26197  nmogtmnf  26409  siilem1  26490  siii  26492  ajmoi  26498  bcsiALT  26830  hhcms  26854  ocval  26931  hsupval  26985  omlsilem  27053  h1de2bi  27205  h1de2ctlem  27206  hosubeq0i  27477  adjmo  27483  nmopgtmnf  27519  nlfnval  27532  nmcopex  27680  nmcfnex  27704  riesz4i  27714  riesz1  27716  riesz2  27717  opsqrlem1  27791  superpos  28005  hatomistici  28013  chpssati  28014  mdsymlem3  28056  3o1cs  28101  3o2cs  28102  3o3cs  28103  spc2ed  28104  brabgaf  28218  f1mptrn  28234  ffsrn  28320  fpwrelmap  28324  ordtrest2NEWlem  28736  qqhval2  28794  esumfsup  28899  esumcvg  28915  cntnevol  29058  ddemeas  29067  dya2icoseg2  29108  dya2iocnei  29112  eulerpartlems  29201  eulerpartlemgvv  29217  eulerpart  29223  cndprobprob  29279  ballotlemsdom  29352  ballotth  29378  ballotlemsdomOLD  29390  ballotthOLD  29416  sgn3da  29420  bnj945  29593  bnj1379  29650  bnj1459  29662  bnj557  29720  bnj571  29725  bnj849  29744  bnj964  29762  bnj978  29768  bnj1018  29781  bnj1020  29782  bnj1033  29786  bnj1175  29821  bnj1398  29851  bnj1417  29858  bnj1523  29888  txpcon  29963  msubco  30177  mclsax  30215  ghomgrp  30316  setinds  30431  dfon2lem7  30442  dfon2lem8  30443  poseq  30498  soseq  30499  frrlem4  30524  frrlem11  30533  nodenselem4  30578  nocvxminlem  30584  nocvxmin  30585  pprodss4v  30656  fullfunfv  30719  altxpsspw  30749  funtransport  30803  fvtransport  30804  funray  30912  fvray  30913  funline  30914  fvline  30916  finminlem  30979  bisym1  31084  onsucconi  31102  onsucsuccmpi  31108  bj-equsal2  31397  bj-xpima1snALT  31518  f1omptsnlem  31702  mptsnunlem  31704  iooelexlt  31729  relowlpssretop  31731  rdgeqoa  31737  wl-lem-nexmo  31860  ptrecube  31904  poimirlem26  31930  poimirlem30  31934  poimir  31937  ismblfin  31945  itg2addnclem  31957  dvasin  31992  sdclem2  32035  totbndbnd  32085  exidresid  32141  isdrngo1  32159  isdrngo2  32161  ispridl2  32235  prtlem11  32406  ax12eq  32481  ax12el  32482  lkr0f  32629  hl2at  32939  dalemswapyz  33190  pclfinclN  33484  osumcllem11N  33500  pexmidlem8N  33511  ltrnnid  33670  mptfcl  35531  fphpd  35628  elmnc  35965  itgoval  35997  arearect  36070  nanorxor  36623  pm11.71  36717  iotavalsb  36754  sbiota1  36755  2uasbanh  36898  eel0TT  37056  eelT00  37057  eelTTT  37058  eelT11  37060  eelT12  37064  eelTT1  37066  eelT01  37067  eel0T1  37068  eelTT  37131  uunT1p1  37141  uun121  37143  uun121p1  37144  un2122  37150  uunTT1  37153  uunTT1p1  37154  uunTT1p2  37155  uunT11  37156  uunT11p1  37157  uunT11p2  37158  uunT12  37159  uunT12p1  37160  uunT12p2  37161  uunT12p3  37162  uunT12p4  37163  uunT12p5  37164  uun111  37165  3anidm12p2  37167  uun123  37168  3impdirp1  37176  undif3VD  37252  ax6e2ndeqVD  37279  2uasbanhVD  37281  ax6e2ndeqALT  37301  iunconlem2  37305  sineq0ALT  37307  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  stoweidlem3  37803  stoweidlem17  37817  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem48  37958  fourierdlem50  37960  fourierdlem51  37961  fourierdlem76  37986  fourierdlem83  37993  fourierdlem87  37997  hoidmvval0  38313  rexrsb  38461  raaan2  38467  afv0nbfvbi  38523  afvfv0bi  38524  afveu  38525  fnbrafvb  38526  afvres  38544  tz6.12-afv  38545  dmfcoafv  38547  afvco2  38548  aovprc  38560  aovrcl  38561  aovmpt4g  38573  fzopred  38589  pfxccat3  38837  pfxccat3a  38840  falseral0  38854  n0snor2el  38862  fun2dmnop  38890  2ffzoeq  38918  structgrssvtx  38956  structgrssiedg  38957  isusgr0  39037  usgrpredgav  39068  usgredg  39079  egrsubgr  39123  nbuhgr  39178  nbusgr  39182  nbuhgr2vtx1edgblem  39184  nbgr0vtxlem  39188  nbgr1vtx  39191  uvtxa01vtx0  39228  cusgrsizeinds  39270  sizusglecusglem2  39280  usgpredgv  39331  usgpredgvALT  39332  ovn0ssdmfun  39387  islinindfis  39864  secval  40089  cscval  40090  cotval  40091
  Copyright terms: Public domain W3C validator