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

Theorem sylbir 204
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 197 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3i  256  ex  423  3ori  1242  ax12olem5  1884  sbi2  2017  sb5rf  2043  ax11eq  2145  ax11el  2146  mo  2178  mo2  2185  2mo  2234  bm1.1  2281  necon1i  2503  sbhypf  2846  vtocl2  2852  vtocl3  2853  reu6  2967  uneqin  3433  inelcm  3522  difin0ss  3533  difprsn1  3770  unissint  3902  intminss  3904  iununi  4002  bm1.3ii  4160  moabex  4248  copsex2g  4270  opelopabt  4293  eusv2nf  4548  reusv3i  4557  reuxfr2d  4573  eldifpw  4582  onminesb  4605  onminsb  4606  onintrab  4608  onnminsb  4611  onsucuni2  4641  tfindsg2  4668  eqrelrel  4804  opeliunxp2  4840  opelrn  4926  issref  5072  ssxpb  5126  dmsn0el  5158  relcoi2  5216  iotanul  5250  dffv2  5608  fnfvrnss  5703  fressnfv  5723  fconst5  5747  fconstfv  5750  zfrep6  5764  f1mpt  5801  isocnv3  5845  f1owe  5866  ovprc  5901  fo1stres  6159  fo2ndres  6160  frxp  6241  reldmtpos  6258  tfrlem5  6412  tfrlem9  6417  tfr2  6430  rdgsuc  6453  oaordi  6560  oeordi  6601  omopthi  6671  fvmptmap  6820  mptelixpg  6869  ener  6924  domtr  6930  snfi  6957  unen  6959  xpf1o  7039  mapen  7041  unxpdomlem3  7085  isinf  7092  frfi  7118  unblem1  7125  unfi  7140  fofinf1o  7153  inf3lem2  7346  inf3lem5  7349  cantnfreslem  7393  cantnfp1lem1  7396  cantnfp1lem3  7398  tcmin  7442  r1ordg  7466  r1ord  7468  rankr1ai  7486  r1val3  7526  bndrank  7529  unbndrank  7530  rankr1b  7552  rankxplim3  7567  tcrank  7570  xpnum  7600  cardmin2  7647  infxpenlem  7657  fseqen  7670  dfac8clem  7675  alephsson  7743  alephfp  7751  dfac4  7765  kmlem6  7797  kmlem8  7799  kmlem9  7800  infpssr  7950  fin1a2lem12  8053  axcc4  8081  axcc4dom  8083  ac6s2  8129  zornn0g  8148  cardidg  8186  unsnen  8191  pwcfsdom  8221  cfpwsdom  8222  gchpwdom  8312  r1tskina  8420  intgru  8452  indpi  8547  nqereu  8569  supsrlem  8749  letrii  8960  infmrcl  9749  dfnn3  9776  zaddcl  10075  uzindOLD  10122  nn0ind  10124  fnn0ind  10127  ublbneg  10318  fzo0end  10931  fzind2  10939  faclbnd4lem1  11322  hashinf  11358  hashfacen  11408  rediv  11632  imdiv  11639  sqr0  11743  fsump1i  12248  cos1bnd  12483  sinltx  12485  rpnnen2lem1  12509  rpnnen2lem2  12510  rpnnen2  12520  odd2np1  12603  gcdcllem1  12706  gcdaddmlem  12723  algfx  12766  odzval  12872  odzdvds  12876  opoe  12880  omoe  12881  opeo  12882  omeo  12883  prmreclem5  12983  mul4sq  13017  imasaddfnlem  13446  mreexexlem4d  13565  lubval  14129  glbval  14134  joinlem  14140  meetlem  14147  clatlem  14232  gictr  14755  cntzval  14813  efgsfo  15064  efgrelexlemb  15075  dprd2da  15293  lssacs  15740  cnfldinv  16421  ocvval  16583  eltopspOLD  16672  tpsexOLD  16673  opnnei  16873  ordtbas2  16937  ordtrest2lem  16949  lmmo  17124  fincmp  17136  txbas  17278  ptcnplem  17331  tx2ndc  17361  hmphtr  17490  fbun  17551  filcon  17594  ptcmplem5  17766  elcncf1di  18415  xrhmeo  18460  phtpycc  18505  copco  18532  pcohtpylem  18533  pcopt  18536  pcopt2  18537  ovolval  18849  iunmbl2  18930  itg2splitlem  19119  cpnfval  19297  plyval  19591  fta1  19704  aaliou2b  19737  ulmdvlem3  19795  radcnvlem2  19806  dvradcnv  19813  reeff1o  19839  sincosq1lem  19881  sincosq2sgn  19883  sincosq4sgn  19885  sinq12ge0  19892  logrncl  19941  eflog  19949  cxpge0  20046  atanf  20192  atanbnd  20238  lgsne0  20588  mul2sq  20620  pntibnd  20758  ostth  20804  isgrpo  20879  ismgm  21003  isrngo  21061  rngoablo2  21105  rngoueqz  21113  isdivrngo  21114  vci  21120  vcex  21152  nmogtmnf  21364  siilem1  21445  siii  21447  ajmoi  21453  bcsiALT  21774  hhcms  21798  ocval  21875  hsupval  21929  omlsilem  21997  h1de2bi  22149  h1de2ctlem  22150  hosubeq0i  22422  adjmo  22428  nmopgtmnf  22464  nlfnval  22477  nmcopex  22625  nmcfnex  22649  riesz4i  22659  riesz1  22661  riesz2  22662  opsqrlem1  22736  superpos  22950  hatomistici  22958  chpssati  22959  mdsymlem3  23001  mdsymi  23007  ballotlemsdom  23086  ballotth  23112  3o1cs  23113  3o2cs  23114  3o3cs  23115  iuninc  23174  cntnevol  23191  xpima  23217  xrsinvgval  23321  logb1  23420  esumcvg  23469  cndprobprob  23656  txpcon  23778  eupath2lem1  23916  ghomgrp  24012  setinds  24204  dfon2lem7  24215  dfon2lem8  24216  nnsinds  24287  nn0sinds  24288  poseq  24323  soseq  24324  wfrlem4  24329  wfrlem12  24337  wfrlem16  24341  wfr2  24343  tfrALTlem  24346  frrlem4  24354  frrlem11  24363  nodenselem4  24408  nocvxminlem  24414  nocvxmin  24415  pprodss4v  24494  fullfunfv  24556  altxpsspw  24582  mptelee  24594  axlowdimlem9  24649  axlowdimlem12  24652  axcontlem2  24664  axcontlem12  24674  funtransport  24725  fvtransport  24726  funray  24834  fvray  24835  funline  24836  fvline  24838  bpolydiflem  24860  bpoly3  24864  bpoly4  24865  bisym1  24929  onsucconi  24947  onsucsuccmpi  24953  itg2addnclem  25002  alneal1a  25106  boxrim  25109  difeqri2  25142  domintrefb  25165  twsymr  25180  prj1b  25181  prj3  25182  fixpc  25196  celsor  25213  domintrefc  25227  dfps2  25391  svli2  25586  vri  25594  inttop2  25617  limptlimpr2lem2  25677  topunfincomp  25692  hdrmp  25808  algi  25829  tartarmap  25990  inttarcar  26003  pgapspf  26154  pgapspf2  26155  gltpntl  26174  bsstr  26230  nbssntr  26231  lppotoslem  26245  lppotos  26246  nbssntrs  26249  finminlem  26333  sdclem2  26554  totbndbnd  26615  exidresid  26671  isdrngo1  26689  isdrngo2  26691  ispridl2  26765  prtlem11  26836  mptfcl  26900  fphpd  27001  elmnc  27443  itgoval  27468  pm11.71  27698  iotavalsb  27735  sbiota1  27736  stoweidlem3  27854  stoweidlem17  27868  rexrsb  28049  raaan2  28055  afv0nbfvbi  28118  afvfv0bi  28119  afveu  28120  fnbrafvb  28121  afvres  28139  tz6.12-afv  28140  dmfcoafv  28142  afvco2  28143  aovprc  28155  aovrcl  28156  aovmpt4g  28168  mpt2xopoveqd  28202  elfznelfzo  28212  injresinjlem  28213  isusgra0  28237  nbgranself2  28284  trlonprop  28340  wlkntrllem5  28348  wlkdvspth  28365  cyclnspth  28375  3v3e3cycl2  28409  3v3e3cycl  28410  4cycl4dv  28412  frgra2v  28422  frgra3vlem1  28423  frgra3vlem2  28424  secval  28470  cscval  28471  cotval  28472  2uasbanh  28625  eel0TT  28783  eelT00  28784  eelTTT  28785  eelT11  28787  eel0121  28789  eelT12  28791  eelTT1  28793  eelT01  28794  eel0T1  28795  eelTT  28859  uunT1p1  28869  uun121  28871  uun121p1  28872  un2122  28878  uunTT1  28881  uunTT1p1  28882  uunTT1p2  28883  uunT11  28884  uunT11p1  28885  uunT11p2  28886  uunT12  28887  uunT12p1  28888  uunT12p2  28889  uunT12p3  28890  uunT12p4  28891  uunT12p5  28892  uun111  28893  3anidm12p2  28895  uun123  28896  3impdirp1  28904  undif3VD  28973  a9e2ndeqVD  29000  2uasbanhVD  29002  a9e2ndeqALT  29023  bnj945  29120  bnj1379  29178  bnj1459  29190  bnj557  29248  bnj571  29253  bnj849  29272  bnj964  29290  bnj978  29296  bnj1018  29309  bnj1020  29310  bnj1033  29314  bnj1175  29349  bnj1398  29379  bnj1417  29386  bnj1523  29416  sbi2NEW7  29538  sb5rfNEW7  29562  a12study5rev  29744  a12study  29754  lkr0f  29906  hl2at  30216  dalemswapyz  30467  pclfinclN  30761  osumcllem11N  30777  pexmidlem8N  30788  ltrnnid  30947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator