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, 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 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  1289  19.38  1649  19.35  1674  equsex  2024  nfeqf2  2027  sbi2  2120  ax12eq  2257  ax12el  2258  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  mo2OLD  2320  2mo  2359  2moOLD  2360  axie2  2416  bm1.1OLD  2427  necon1bi  2676  necon1i  2685  sbhypf  3142  vtocl2  3148  vtocl3  3149  reu6  3274  uneqin  3734  inelcm  3867  difin0ss  3880  difprsn1  4151  tppreqb  4156  unissint  4296  intminss  4298  iununi  4400  bm1.3ii  4561  eusv2nf  4635  reusv3i  4644  reuxfr2d  4660  moabex  4696  copsex2g  4725  opelopabt  4749  eqrelrel  5094  opeliunxp2  5131  opelrn  5224  issref  5370  ssxpb  5431  xpima  5439  xpimasn  5442  dmsn0el  5467  relcoi2  5525  iotanul  5556  dffv2  5931  fnfvrnss  6044  fressnfv  6070  fconst5  6113  fconstfvOLD  6119  f1mpt  6154  isocnv3  6213  f1owe  6234  ovprc  6311  onminesb  6618  onminsb  6619  onintrab  6621  onnminsb  6624  onsucuni2  6654  tfindsg2  6681  zfrep6  6753  fo1stres  6809  fo2ndres  6810  bropopvvv  6865  frxp  6895  mpt2xopoveqd  6951  reldmtpos  6965  tfrlem5  7051  tfrlem9  7056  tfr2  7069  rdgsuc  7092  oaordi  7197  oeordi  7238  omopthi  7308  fvmptmap  7457  mptelixpg  7508  ener  7564  domtr  7570  snfi  7598  unen  7600  xpf1o  7681  mapen  7683  unxpdomlem3  7728  isinf  7735  frfi  7767  unblem1  7774  unfi  7789  fofinf1o  7803  fsuppun  7850  inf3lem2  8049  inf3lem5  8052  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  tcmin  8175  r1ordg  8199  r1ord  8201  rankr1ai  8219  r1val3  8259  bndrank  8262  unbndrank  8263  rankr1b  8285  rankxplim3  8302  tcrank  8305  xpnum  8335  cardmin2  8382  infxpenlem  8394  fseqen  8411  dfac8clem  8416  alephsson  8484  alephfp  8492  dfac4  8506  kmlem6  8538  kmlem8  8540  kmlem9  8541  infpssr  8691  fin1a2lem12  8794  axcc4  8822  axcc4dom  8824  ac6s2  8869  zornn0g  8888  cardidg  8926  unsnen  8931  pwcfsdom  8961  cfpwsdom  8962  gchpwdom  9051  r1tskina  9163  intgru  9195  indpi  9288  nqereu  9310  supsrlem  9491  letrii  9712  infmrcl  10528  dfnn3  10556  zaddcl  10910  uzindOLD  10963  nn0ind  10965  fnn0ind  10968  ublbneg  11175  nn01to3  11184  fz0  11710  fzo1fzo0n0  11843  elfzom1elp1fzo  11862  fzo0end  11883  elfznelfzo  11894  fzind2  11903  injresinjlem  11904  fleqceilz  11960  fsuppmapnn0fiubex  12077  faclbnd4lem1  12350  hashinf  12389  hasheqf1oi  12403  hashgt0elex  12445  hashfacen  12482  hash2prde  12495  lswcl  12568  lswccats1fst  12618  swrdlsw  12656  swrdswrdlem  12663  swrdccatin12lem3  12694  swrdccat3  12696  swrdccat3blem  12699  cshwsublen  12746  cshwidxmod  12753  repswcshw  12759  cshw1  12769  rediv  12943  imdiv  12950  sqrt0  13054  fsump1i  13563  modfsummods  13586  cos1bnd  13799  sinltx  13801  rpnnen2lem1  13825  rpnnen2lem2  13826  rpnnen2  13836  odd2np1  13923  gcdcllem1  14026  gcdaddmlem  14043  algfx  14086  odzval  14195  odzdvds  14199  opoe  14212  omoe  14213  opeo  14214  omeo  14215  prmreclem5  14315  mul4sq  14349  imasaddfnlem  14802  mreexexlem4d  14921  joindmss  15511  meetdmss  15525  gictr  16197  cntzval  16233  symg2bas  16297  efgsfo  16631  efgrelexlemb  16642  dprddomcld  16906  dprdsubg  16945  dprd2da  16965  lssacs  17487  cnfldinv  18323  ocvval  18571  dmatmul  18872  mdetfval1  18965  mndifsplit  19011  fvmptnn04if  19223  eltopspOLD  19292  tpsexOLD  19293  opnnei  19494  ordtbas2  19565  ordtrest2lem  19577  lmmo  19754  fincmp  19766  bwth  19783  txbas  19941  ptcnplem  19995  tx2ndc  20025  hmphtr  20157  fbun  20214  filcon  20257  ptcmplem5  20429  cnextcn  20440  utoptop  20610  ucncn  20661  metustOLD  20943  metust  20944  cfilucfilOLD  20945  cfilucfil  20946  elcncf1di  21272  xrhmeo  21319  phtpycc  21364  copco  21391  pcohtpylem  21392  pcopt  21395  pcopt2  21396  ovolval  21758  iunmbl2  21840  itg2splitlem  22028  cpnfval  22208  plyval  22463  fta1  22576  aaliou2b  22609  ulmdvlem3  22669  radcnvlem2  22681  dvradcnv  22688  reeff1o  22714  sincosq1lem  22762  sincosq2sgn  22764  sincosq4sgn  22766  sinq12ge0  22773  logrncl  22827  eflog  22836  cxpge0  22936  atanf  23083  atanbnd  23129  lgsne0  23480  mul2sq  23512  pntibnd  23650  ostth  23696  mptelee  24070  axlowdimlem9  24125  axlowdimlem12  24128  axcontlem2  24140  axcontlem12  24150  isusgra0  24219  usgraop  24222  usgraedg4  24259  nbusgra  24300  nbgranself2  24308  wlkn0  24399  wlkcpr  24401  wlkntrllem3  24435  spthonepeq  24461  wlkdvspth  24482  cyclnspth  24503  3v3e3cycl2  24536  3v3e3cycl  24537  4cycl4dv  24539  2wlkeq  24579  usg2wlkeq  24580  clwwlknprop  24644  clwwisshclww  24679  wlklenvclwlk  24711  2wlkonot3v  24747  2spthonot3v  24748  2spontn0vne  24759  vdgrf  24770  usgfiregdegfi  24783  nbhashuvtx1  24787  eupath2lem1  24849  frgra3vlem1  24872  frgra3vlem2  24873  frgrancvvdeqlem2  24903  frgrancvvdeqlem3  24904  frgrancvvdeqlemB  24910  frgrancvvdeqlemC  24911  frgrawopreglem5  24920  usgreghash2spot  24941  frgrareg  24989  frgraregord013  24990  friendshipgt3  24993  isgrpo  25070  ismgmOLD  25194  isrngo  25252  rngoablo2  25296  rngoueqz  25304  isdivrngo  25305  vci  25313  vcex  25345  nmogtmnf  25557  siilem1  25638  siii  25640  ajmoi  25646  bcsiALT  25968  hhcms  25992  ocval  26070  hsupval  26124  omlsilem  26192  h1de2bi  26344  h1de2ctlem  26345  hosubeq0i  26617  adjmo  26623  nmopgtmnf  26659  nlfnval  26672  nmcopex  26820  nmcfnex  26844  riesz4i  26854  riesz1  26856  riesz2  26857  opsqrlem1  26931  superpos  27145  hatomistici  27153  chpssati  27154  mdsymlem3  27196  3o1cs  27241  3o2cs  27242  3o3cs  27243  spc2ed  27244  ffsrn  27424  fpwrelmap  27428  ordtrest2NEWlem  27777  qqhval2  27836  logb1  27892  esumfsup  27949  esumcvg  27965  cntnevol  28072  ddemeas  28081  dya2icoseg2  28122  dya2iocnei  28126  eulerpartlems  28172  eulerpartlemgvv  28188  eulerpart  28194  cndprobprob  28250  ballotlemsdom  28323  ballotth  28349  sgn3da  28353  igamf  28466  igamcl  28467  txpcon  28550  msubco  28764  mclsax  28802  ghomgrp  28903  setinds  29185  dfon2lem7  29196  dfon2lem8  29197  nnsinds  29272  nn0sinds  29273  poseq  29308  soseq  29309  wfrlem4  29321  wfrlem12  29329  wfrlem16  29333  wfr2  29335  frrlem4  29365  frrlem11  29374  nodenselem4  29419  nocvxminlem  29425  nocvxmin  29426  pprodss4v  29509  fullfunfv  29572  altxpsspw  29602  funtransport  29656  fvtransport  29657  funray  29765  fvray  29766  funline  29767  fvline  29769  bpolydiflem  29791  bpoly3  29795  bpoly4  29796  bisym1  29859  onsucconi  29877  onsucsuccmpi  29883  wl-lem-nexmo  29991  ismblfin  30030  itg2addnclem  30041  dvasin  30078  finminlem  30111  sdclem2  30210  totbndbnd  30260  exidresid  30316  isdrngo1  30334  isdrngo2  30336  ispridl2  30410  prtlem11  30582  mptfcl  30627  fphpd  30725  elmnc  31061  itgoval  31086  arearect  31159  nanorxor  31161  lcmledvds  31181  pm11.71  31257  iotavalsb  31294  sbiota1  31295  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  stoweidlem3  31674  stoweidlem17  31688  fourierdlem42  31820  fourierdlem48  31826  fourierdlem50  31828  fourierdlem51  31829  fourierdlem76  31854  fourierdlem83  31861  fourierdlem87  31865  rexrsb  32012  raaan2  32018  afv0nbfvbi  32074  afvfv0bi  32075  afveu  32076  fnbrafvb  32077  afvres  32095  tz6.12-afv  32096  dmfcoafv  32098  afvco2  32099  aovprc  32111  aovrcl  32112  aovmpt4g  32124  2ffzoeq  32179  usgpredgv  32237  usgpredgvALT  32238  ovn0ssdmfun  32293  islinindfis  32785  secval  32876  cscval  32877  cotval  32878  2uasbanh  33067  eel0TT  33225  eelT00  33226  eelTTT  33227  eelT11  33229  eelT12  33233  eelTT1  33235  eelT01  33236  eel0T1  33237  eelTT  33301  uunT1p1  33311  uun121  33313  uun121p1  33314  un2122  33320  uunTT1  33323  uunTT1p1  33324  uunTT1p2  33325  uunT11  33326  uunT11p1  33327  uunT11p2  33328  uunT12  33329  uunT12p1  33330  uunT12p2  33331  uunT12p3  33332  uunT12p4  33333  uunT12p5  33334  uun111  33335  3anidm12p2  33337  uun123  33338  3impdirp1  33346  undif3VD  33415  ax6e2ndeqVD  33442  2uasbanhVD  33444  ax6e2ndeqALT  33464  iunconlem2  33468  sineq0ALT  33470  bnj945  33565  bnj1379  33622  bnj1459  33634  bnj557  33692  bnj571  33697  bnj849  33716  bnj964  33734  bnj978  33740  bnj1018  33753  bnj1020  33754  bnj1033  33758  bnj1175  33793  bnj1398  33823  bnj1417  33830  bnj1523  33860  bj-equsexv  34060  bj-equsexvv  34061  bj-equsal2  34146  bj-xpima1snALT  34262  lkr0f  34559  hl2at  34869  dalemswapyz  35120  pclfinclN  35414  osumcllem11N  35430  pexmidlem8N  35441  ltrnnid  35600
  Copyright terms: Public domain W3C validator