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  1709  19.35  1734  equsex  2093  nfeqf2  2097  sbi2  2188  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  2mo  2351  2moOLD  2352  axie2  2402  bm1.1OLD  2413  necon1bi  2664  necon1i  2673  sbhypf  3134  vtocl2  3140  vtocl3  3141  reu6  3266  uneqin  3730  inelcm  3853  difin0ss  3867  difprsn1  4139  tppreqb  4144  unissint  4283  intminss  4285  iununi  4390  bm1.3ii  4551  eusv2nf  4623  reusv3i  4632  reuxfr2d  4645  moabex  4681  copsex2g  4709  opelopabt  4733  eqrelrel  4956  opeliunxp2  4993  opelrn  5086  issref  5233  ssxpb  5291  xpima  5299  xpimasn  5302  dmsn0el  5325  relcoi2  5383  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  mpt2xopoveqd  6975  reldmtpos  6989  wfrlem4  7047  wfrlem12  7055  wfrlem16  7059  wfr2  7063  tfrlem5  7106  tfrlem9  7111  tfr2  7124  rdgsuc  7150  oaordi  7255  oeordi  7296  omopthi  7366  fvmptmap  7516  mptelixpg  7567  ener  7623  domtr  7629  snfi  7657  unen  7659  xpf1o  7740  mapen  7742  unxpdomlem3  7784  isinf  7791  frfi  7822  unblem1  7829  unfi  7844  fofinf1o  7858  fsuppun  7908  inf3lem2  8134  inf3lem5  8137  cantnfp1lem1  8182  cantnfp1lem3  8184  tcmin  8224  r1ordg  8248  r1ord  8250  rankr1ai  8268  r1val3  8308  bndrank  8311  unbndrank  8312  rankr1b  8334  rankxplim3  8351  tcrank  8354  xpnum  8384  cardmin2  8431  infxpenlem  8443  fseqen  8456  dfac8clem  8461  alephsson  8529  alephfp  8537  dfac4  8551  kmlem6  8583  kmlem8  8585  kmlem9  8586  infpssr  8736  fin1a2lem12  8839  axcc4  8867  axcc4dom  8869  ac6s2  8914  zornn0g  8933  cardidg  8971  unsnen  8976  pwcfsdom  9006  cfpwsdom  9007  gchpwdom  9094  r1tskina  9206  intgru  9238  indpi  9331  nqereu  9353  supsrlem  9534  letrii  9758  infmrclOLD  10593  dfnn3  10623  zaddcl  10977  nn0ind  11030  fnn0ind  11034  ublbneg  11248  nn01to3  11257  infmrp1  11634  fz0  11812  fzo1fzo0n0  11955  elfzom1elp1fzo  11978  fzo0end  12000  elfznelfzo  12011  fzind2  12020  injresinjlem  12021  fleqceilz  12078  nnsinds  12197  nn0sinds  12198  fsuppmapnn0fiubex  12201  faclbnd4lem1  12475  hashinf  12517  hasheqf1oi  12531  hashgt0elex  12575  hashfacen  12612  hash2prde  12625  swrdn0  12771  swrdlsw  12793  swrdswrdlem  12800  swrdccatin12lem3  12831  swrdccat3  12833  swrdccat3blem  12836  cshwsublen  12883  cshwidxmod  12890  repswcshw  12896  cshw1  12906  trclun  13057  dmtrclfv  13061  rediv  13173  imdiv  13180  sqrt0  13284  fsump1i  13808  modfsummods  13831  bpolydiflem  14085  bpoly3  14089  bpoly4  14090  cos1bnd  14219  sinltx  14221  rpnnen2lem1  14245  rpnnen2lem2  14246  rpnnen2  14256  odd2np1  14343  gcdcllem1  14447  gcdaddmlem  14466  algfx  14510  lcmledvds  14529  lcmsledvdsOLD  14550  lcmfunsnlem  14576  lcmfun  14580  coprmprod  14640  coprmproddvdslem  14641  odzval  14696  odzdvds  14700  opoe  14715  omoe  14716  opeo  14717  omeo  14718  prmreclem5  14818  mul4sq  14852  prmgaplem5  14979  prmgaplem6  14980  imasaddfnlem  15376  mreexexlem4d  15495  joindmss  16195  meetdmss  16209  gictr  16881  cntzval  16917  symg2bas  16981  efgsfo  17315  efgrelexlemb  17326  dprddomcld  17559  dprdsubg  17583  dprd2da  17601  lssacs  18116  cnfldinv  18925  ocvval  19152  dmatmul  19444  mdetfval1  19537  mndifsplit  19583  fvmptnn04if  19795  opnnei  20058  ordtbas2  20129  ordtrest2lem  20141  lmmo  20318  fincmp  20330  bwth  20347  txbas  20504  ptcnplem  20558  tx2ndc  20588  hmphtr  20720  fbun  20777  filcon  20820  ptcmplem5  20993  cnextcn  21004  utoptop  21171  ucncn  21222  metust  21495  cfilucfil  21496  elcncf1di  21814  xrhmeo  21861  phtpycc  21906  copco  21933  pcohtpylem  21934  pcopt  21937  pcopt2  21938  ovolval  22296  iunmbl2  22378  itg2splitlem  22574  cpnfval  22754  plyval  23006  fta1  23120  aaliou2b  23153  ulmdvlem3  23213  radcnvlem2  23225  dvradcnv  23232  reeff1o  23258  sincosq1lem  23308  sincosq2sgn  23310  sincosq4sgn  23312  sinq12ge0  23319  logrncl  23373  eflog  23382  cxpge0  23484  logb1  23562  atanf  23662  atanbnd  23708  igamf  23832  igamcl  23833  lgsne0  24115  mul2sq  24147  pntibnd  24285  ostth  24331  mptelee  24762  axlowdimlem9  24817  axlowdimlem12  24820  axcontlem2  24832  axcontlem12  24842  isusgra0  24911  usgraop  24914  usgraedg4  24951  nbusgra  24992  nbgranself2  25000  wlkn0  25091  wlkcpr  25093  wlkntrllem3  25127  spthonepeq  25153  wlkdvspth  25174  cyclnspth  25195  3v3e3cycl2  25228  3v3e3cycl  25229  4cycl4dv  25231  2wlkeq  25271  usg2wlkeq  25272  clwwlknprop  25336  clwwisshclww  25371  wlklenvclwlk  25403  2wlkonot3v  25439  2spthonot3v  25440  2spontn0vne  25451  vdgrf  25462  usgfiregdegfi  25475  nbhashuvtx1  25479  eupath2lem1  25541  frgra3vlem1  25564  frgra3vlem2  25565  frgrancvvdeqlem2  25595  frgrancvvdeqlem3  25596  frgrancvvdeqlemB  25602  frgrancvvdeqlemC  25603  frgrawopreglem5  25612  usgreghash2spot  25633  frgrareg  25681  frgraregord013  25682  friendshipgt3  25685  isgrpo  25760  ismgmOLD  25884  isrngo  25942  rngoablo2  25986  rngoueqz  25994  isdivrngo  25995  vci  26003  vcex  26035  nmogtmnf  26247  siilem1  26328  siii  26330  ajmoi  26336  bcsiALT  26658  hhcms  26682  ocval  26759  hsupval  26813  omlsilem  26881  h1de2bi  27033  h1de2ctlem  27034  hosubeq0i  27305  adjmo  27311  nmopgtmnf  27347  nlfnval  27360  nmcopex  27508  nmcfnex  27532  riesz4i  27542  riesz1  27544  riesz2  27545  opsqrlem1  27619  superpos  27833  hatomistici  27841  chpssati  27842  mdsymlem3  27884  3o1cs  27929  3o2cs  27930  3o3cs  27931  spc2ed  27932  brabgaf  28046  elsnxp  28054  f1mptrn  28063  ffsrn  28148  fpwrelmap  28152  ordtrest2NEWlem  28558  qqhval2  28616  esumfsup  28721  esumcvg  28737  cntnevol  28880  ddemeas  28889  dya2icoseg2  28930  dya2iocnei  28934  eulerpartlems  29010  eulerpartlemgvv  29026  eulerpart  29032  cndprobprob  29088  ballotlemsdom  29161  ballotth  29187  sgn3da  29191  bnj945  29364  bnj1379  29421  bnj1459  29433  bnj557  29491  bnj571  29496  bnj849  29515  bnj964  29533  bnj978  29539  bnj1018  29552  bnj1020  29553  bnj1033  29557  bnj1175  29592  bnj1398  29622  bnj1417  29629  bnj1523  29659  txpcon  29734  msubco  29948  mclsax  29986  ghomgrp  30087  setinds  30202  dfon2lem7  30213  dfon2lem8  30214  poseq  30269  soseq  30270  frrlem4  30295  frrlem11  30304  nodenselem4  30349  nocvxminlem  30355  nocvxmin  30356  pprodss4v  30427  fullfunfv  30490  altxpsspw  30520  funtransport  30574  fvtransport  30575  funray  30683  fvray  30684  funline  30685  fvline  30687  finminlem  30750  bisym1  30855  onsucconi  30873  onsucsuccmpi  30879  bj-equsal2  31169  bj-xpima1snALT  31290  f1omptsnlem  31463  mptsnunlem  31465  iooelexlt  31490  relowlpssretop  31492  wl-lem-nexmo  31594  ptrecube  31634  poimirlem26  31660  poimirlem30  31664  poimir  31667  ismblfin  31675  itg2addnclem  31687  dvasin  31722  sdclem2  31765  totbndbnd  31815  exidresid  31871  isdrngo1  31889  isdrngo2  31891  ispridl2  31965  prtlem11  32136  ax12eq  32211  ax12el  32212  lkr0f  32359  hl2at  32669  dalemswapyz  32920  pclfinclN  33214  osumcllem11N  33230  pexmidlem8N  33241  ltrnnid  33400  mptfcl  35261  fphpd  35358  elmnc  35691  itgoval  35716  arearect  35789  nanorxor  36280  pm11.71  36374  iotavalsb  36411  sbiota1  36412  2uasbanh  36555  eel0TT  36713  eelT00  36714  eelTTT  36715  eelT11  36717  eelT12  36721  eelTT1  36723  eelT01  36724  eel0T1  36725  eelTT  36788  uunT1p1  36798  uun121  36800  uun121p1  36801  un2122  36807  uunTT1  36810  uunTT1p1  36811  uunTT1p2  36812  uunT11  36813  uunT11p1  36814  uunT11p2  36815  uunT12  36816  uunT12p1  36817  uunT12p2  36818  uunT12p3  36819  uunT12p4  36820  uunT12p5  36821  uun111  36822  3anidm12p2  36824  uun123  36825  3impdirp1  36833  undif3VD  36909  ax6e2ndeqVD  36936  2uasbanhVD  36938  ax6e2ndeqALT  36958  iunconlem2  36962  sineq0ALT  36964  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  stoweidlem3  37422  stoweidlem17  37436  fourierdlem42  37570  fourierdlem48  37576  fourierdlem50  37578  fourierdlem51  37579  fourierdlem76  37604  fourierdlem83  37611  fourierdlem87  37615  rexrsb  37971  raaan2  37977  afv0nbfvbi  38033  afvfv0bi  38034  afveu  38035  fnbrafvb  38036  afvres  38054  tz6.12-afv  38055  dmfcoafv  38057  afvco2  38058  aovprc  38070  aovrcl  38071  aovmpt4g  38083  fzopred  38099  pfxccat3  38347  pfxccat3a  38350  2ffzoeq  38403  usgpredgv  38459  usgpredgvALT  38460  ovn0ssdmfun  38515  islinindfis  38992  secval  39218  cscval  39219  cotval  39220
  Copyright terms: Public domain W3C validator