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  1278  19.38  1629  19.35  1654  equsex  1986  nfeqf2  1989  sbi2  2085  sb5rfOLD  2121  ax12eq  2242  ax12el  2243  mo2v  2260  mo2vOLD  2261  mo2vOLDOLD  2262  moOLD  2305  mo2OLD  2314  2mo  2360  2moOLD  2361  2moOLDOLD  2362  axie2  2418  bm1.1OLD  2428  necon1i  2679  sbhypf  3040  vtocl2  3046  vtocl3  3047  reu6  3169  uneqin  3622  inelcm  3754  difin0ss  3766  difprsn1  4031  tppreqb  4035  unissint  4173  intminss  4175  iununi  4276  bm1.3ii  4437  eusv2nf  4511  reusv3i  4520  reuxfr2d  4536  moabex  4572  copsex2g  4600  opelopabt  4622  eqrelrel  4962  opeliunxp2  4999  opelrn  5092  issref  5232  ssxpb  5293  xpima  5301  xpimasn  5304  dmsn0el  5329  relcoi2  5386  iotanul  5417  dffv2  5785  fnfvrnss  5892  fressnfv  5917  fconst5  5956  fconstfv  5961  f1mpt  5995  isocnv3  6044  f1owe  6065  ovprc  6139  onminesb  6430  onminsb  6431  onintrab  6433  onnminsb  6436  onsucuni2  6466  tfindsg2  6493  zfrep6  6566  fo1stres  6621  fo2ndres  6622  bropopvvv  6674  frxp  6703  mpt2xopoveqd  6759  reldmtpos  6774  tfrlem5  6860  tfrlem9  6865  tfr2  6878  rdgsuc  6901  oaordi  7006  oeordi  7047  omopthi  7117  fvmptmap  7270  mptelixpg  7321  ener  7377  domtr  7383  snfi  7411  unen  7413  xpf1o  7494  mapen  7496  unxpdomlem3  7540  isinf  7547  frfi  7578  unblem1  7585  unfi  7600  fofinf1o  7613  fsuppun  7660  inf3lem2  7856  inf3lem5  7859  cantnfp1lem1  7907  cantnfp1lem3  7909  cantnfp1lem1OLD  7933  cantnfp1lem3OLD  7935  tcmin  7982  r1ordg  8006  r1ord  8008  rankr1ai  8026  r1val3  8066  bndrank  8069  unbndrank  8070  rankr1b  8092  rankxplim3  8109  tcrank  8112  xpnum  8142  cardmin2  8189  infxpenlem  8201  fseqen  8218  dfac8clem  8223  alephsson  8291  alephfp  8299  dfac4  8313  kmlem6  8345  kmlem8  8347  kmlem9  8348  infpssr  8498  fin1a2lem12  8601  axcc4  8629  axcc4dom  8631  ac6s2  8676  zornn0g  8695  cardidg  8733  unsnen  8738  pwcfsdom  8768  cfpwsdom  8769  gchpwdom  8858  r1tskina  8970  intgru  9002  indpi  9097  nqereu  9119  supsrlem  9299  letrii  9520  infmrcl  10330  dfnn3  10357  zaddcl  10706  uzindOLD  10757  nn0ind  10759  fnn0ind  10762  ublbneg  10960  fz0  11486  fzo1fzo0n0  11609  fzo0end  11640  elfznelfzo  11651  fzind2  11658  injresinjlem  11659  fleqceilz  11714  faclbnd4lem1  12090  hashinf  12129  hasheqf1oi  12143  hashgt0elex  12180  hash2prde  12200  hashfacen  12228  lswcl  12291  swrdlsw  12367  swrdswrdlem  12374  swrdccatin12lem3  12402  swrdccat3  12404  swrdccat3blem  12407  cshwsublen  12454  cshwidxmod  12461  repswcshw  12467  cshw1  12477  rediv  12641  imdiv  12648  sqr0  12752  fsump1i  13257  cos1bnd  13492  sinltx  13494  rpnnen2lem1  13518  rpnnen2lem2  13519  rpnnen2  13529  odd2np1  13613  gcdcllem1  13716  gcdaddmlem  13733  algfx  13776  odzval  13884  odzdvds  13888  opoe  13899  omoe  13900  opeo  13901  omeo  13902  prmreclem5  14002  mul4sq  14036  imasaddfnlem  14487  mreexexlem4d  14606  joindmss  15198  meetdmss  15212  gictr  15824  cntzval  15860  symg2bas  15924  efgsfo  16257  efgrelexlemb  16268  dprddomcld  16505  dprdsubg  16543  dprd2da  16563  lssacs  17070  cnfldinv  17869  ocvval  18114  mdetfval1  18423  mndifsplit  18464  eltopspOLD  18545  tpsexOLD  18546  opnnei  18746  ordtbas2  18817  ordtrest2lem  18829  lmmo  19006  fincmp  19018  bwth  19035  txbas  19162  ptcnplem  19216  tx2ndc  19246  hmphtr  19378  fbun  19435  filcon  19478  ptcmplem5  19650  cnextcn  19661  utoptop  19831  restutopopn  19835  ucncn  19882  metustOLD  20164  metust  20165  cfilucfilOLD  20166  cfilucfil  20167  elcncf1di  20493  xrhmeo  20540  phtpycc  20585  copco  20612  pcohtpylem  20613  pcopt  20616  pcopt2  20617  ovolval  20979  iunmbl2  21060  itg2splitlem  21248  cpnfval  21428  plyval  21683  fta1  21796  aaliou2b  21829  ulmdvlem3  21889  radcnvlem2  21901  dvradcnv  21908  reeff1o  21934  sincosq1lem  21981  sincosq2sgn  21983  sincosq4sgn  21985  sinq12ge0  21992  logrncl  22041  eflog  22050  cxpge0  22150  atanf  22297  atanbnd  22343  lgsne0  22694  mul2sq  22726  pntibnd  22864  ostth  22910  mptelee  23163  axlowdimlem9  23218  axlowdimlem12  23221  axcontlem2  23233  axcontlem12  23243  isusgra0  23297  usgraedg4  23327  nbusgra  23361  nbgranself2  23369  wlkntrllem3  23482  spthonepeq  23508  wlkdvspth  23529  cyclnspth  23539  3v3e3cycl2  23572  3v3e3cycl  23573  4cycl4dv  23575  vdgrf  23590  eupath2lem1  23620  isgrpo  23705  ismgm  23829  isrngo  23887  rngoablo2  23931  rngoueqz  23939  isdivrngo  23940  vci  23948  vcex  23980  nmogtmnf  24192  siilem1  24273  siii  24275  ajmoi  24281  bcsiALT  24603  hhcms  24627  ocval  24705  hsupval  24759  omlsilem  24827  h1de2bi  24979  h1de2ctlem  24980  hosubeq0i  25252  adjmo  25258  nmopgtmnf  25294  nlfnval  25307  nmcopex  25455  nmcfnex  25479  riesz4i  25489  riesz1  25491  riesz2  25492  opsqrlem1  25566  superpos  25780  hatomistici  25788  chpssati  25789  mdsymlem3  25831  mdsymi  25837  3o1cs  25876  3o2cs  25877  3o3cs  25878  ffsrn  26051  fpwrelmap  26055  ordtrest2NEWlem  26374  qqhval2  26433  logb1  26484  esumfsup  26541  esumcvg  26557  cntnevol  26664  ddemeas  26674  dya2icoseg2  26715  dya2iocnei  26719  eulerpartlems  26765  eulerpartlemgvv  26781  eulerpart  26787  cndprobprob  26843  ballotlemsdom  26916  ballotth  26942  sgn3da  26946  igamf  27059  igamcl  27060  txpcon  27143  ghomgrp  27331  setinds  27613  dfon2lem7  27624  dfon2lem8  27625  nnsinds  27700  nn0sinds  27701  poseq  27736  soseq  27737  wfrlem4  27749  wfrlem12  27757  wfrlem16  27761  wfr2  27763  frrlem4  27793  frrlem11  27802  nodenselem4  27847  nocvxminlem  27853  nocvxmin  27854  pprodss4v  27937  fullfunfv  28000  altxpsspw  28030  funtransport  28084  fvtransport  28085  funray  28193  fvray  28194  funline  28195  fvline  28197  bpolydiflem  28219  bpoly3  28223  bpoly4  28224  bisym1  28287  onsucconi  28305  onsucsuccmpi  28311  wl-lem-nexmo  28418  ismblfin  28458  itg2addnclem  28469  dvasin  28506  finminlem  28539  sdclem2  28664  totbndbnd  28714  exidresid  28770  isdrngo1  28788  isdrngo2  28790  ispridl2  28864  prtlem11  29037  mptfcl  29082  fphpd  29181  elmnc  29519  itgoval  29544  arearect  29617  pm11.71  29676  iotavalsb  29713  sbiota1  29714  stoweidlem3  29824  stoweidlem17  29838  rexrsb  30019  raaan2  30025  afv0nbfvbi  30083  afvfv0bi  30084  afveu  30085  fnbrafvb  30086  afvres  30104  tz6.12-afv  30105  dmfcoafv  30107  afvco2  30108  aovprc  30120  aovrcl  30121  aovmpt4g  30133  nn01to3  30213  2ffzoeq  30240  modfsummods  30270  lswccats1fst  30288  wlkn0  30305  2wlkeq  30314  usg2wlkeq  30315  wlkcpr  30316  2wlkonot3v  30420  2spthonot3v  30421  2spontn0vne  30432  clwwlknprop  30461  clwwisshclww  30497  wlkp1lenfislenp  30538  usgfiregdegfi  30554  nbhashuvtx1  30559  frgra3vlem1  30618  frgra3vlem2  30619  frgrancvvdeqlem2  30650  frgrancvvdeqlem3  30651  frgrancvvdeqlemB  30657  frgrancvvdeqlemC  30658  frgrawopreglem5  30667  usgreghash2spot  30688  frgrareg  30736  frgraregord013  30737  friendshipgt3  30740  fsuppmapnn0fiubex  30830  dmatmul  30915  islinindfis  30980  pmattomply1f1  31137  secval  31178  cscval  31179  cotval  31180  2uasbanh  31366  eel0TT  31524  eelT00  31525  eelTTT  31526  eelT11  31528  eelT12  31532  eelTT1  31534  eelT01  31535  eel0T1  31536  eelTT  31600  uunT1p1  31610  uun121  31612  uun121p1  31613  un2122  31619  uunTT1  31622  uunTT1p1  31623  uunTT1p2  31624  uunT11  31625  uunT11p1  31626  uunT11p2  31627  uunT12  31628  uunT12p1  31629  uunT12p2  31630  uunT12p3  31631  uunT12p4  31632  uunT12p5  31633  uun111  31634  3anidm12p2  31636  uun123  31637  3impdirp1  31645  undif3VD  31714  ax6e2ndeqVD  31741  2uasbanhVD  31743  ax6e2ndeqALT  31763  iunconlem2  31767  sineq0ALT  31769  bnj945  31863  bnj1379  31920  bnj1459  31932  bnj557  31990  bnj571  31995  bnj849  32014  bnj964  32032  bnj978  32038  bnj1018  32051  bnj1020  32052  bnj1033  32056  bnj1175  32091  bnj1398  32121  bnj1417  32128  bnj1523  32158  bj-equsexv  32344  bj-equsal2  32429  bj-xpima1snALT  32545  lkr0f  32835  hl2at  33145  dalemswapyz  33396  pclfinclN  33690  osumcllem11N  33706  pexmidlem8N  33717  ltrnnid  33876
  Copyright terms: Public domain W3C validator