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  24205  dfon2lem7  24216  dfon2lem8  24217  nnsinds  24288  nn0sinds  24289  poseq  24324  soseq  24325  wfrlem4  24330  wfrlem12  24338  wfrlem16  24342  wfr2  24344  tfrALTlem  24347  frrlem4  24355  frrlem11  24364  nodenselem4  24409  nocvxminlem  24415  nocvxmin  24416  pprodss4v  24495  fullfunfv  24557  altxpsspw  24583  mptelee  24595  axlowdimlem9  24650  axlowdimlem12  24653  axcontlem2  24665  axcontlem12  24675  funtransport  24726  fvtransport  24727  funray  24835  fvray  24836  funline  24837  fvline  24839  bpolydiflem  24861  bpoly3  24865  bpoly4  24866  bisym1  24930  onsucconi  24948  onsucsuccmpi  24954  itg2addnclem  25003  alneal1a  25107  boxrim  25110  difeqri2  25143  domintrefb  25166  twsymr  25181  prj1b  25182  prj3  25183  fixpc  25197  celsor  25214  domintrefc  25228  dfps2  25392  svli2  25587  vri  25595  inttop2  25618  limptlimpr2lem2  25678  topunfincomp  25693  hdrmp  25809  algi  25830  tartarmap  25991  inttarcar  26004  pgapspf  26155  pgapspf2  26156  gltpntl  26175  bsstr  26231  nbssntr  26232  lppotoslem  26246  lppotos  26247  nbssntrs  26250  finminlem  26334  sdclem2  26555  totbndbnd  26616  exidresid  26672  isdrngo1  26690  isdrngo2  26692  ispridl2  26766  prtlem11  26837  mptfcl  26901  fphpd  27002  elmnc  27444  itgoval  27469  pm11.71  27699  iotavalsb  27736  sbiota1  27737  stoweidlem3  27855  stoweidlem17  27869  rexrsb  28050  raaan2  28056  afv0nbfvbi  28119  afvfv0bi  28120  afveu  28121  fnbrafvb  28122  afvres  28140  tz6.12-afv  28141  dmfcoafv  28143  afvco2  28144  aovprc  28156  aovrcl  28157  aovmpt4g  28169  mpt2xopoveqd  28203  elfznelfzo  28213  injresinjlem  28214  isusgra0  28238  nbgranself2  28285  trlonprop  28341  wlkntrllem5  28349  wlkdvspth  28366  cyclnspth  28376  3v3e3cycl2  28410  3v3e3cycl  28411  4cycl4dv  28413  frgra2v  28423  frgra3vlem1  28424  frgra3vlem2  28425  secval  28471  cscval  28472  cotval  28473  2uasbanh  28626  eel0TT  28784  eelT00  28785  eelTTT  28786  eelT11  28788  eel0121  28790  eelT12  28792  eelTT1  28794  eelT01  28795  eel0T1  28796  eelTT  28860  uunT1p1  28870  uun121  28872  uun121p1  28873  un2122  28879  uunTT1  28882  uunTT1p1  28883  uunTT1p2  28884  uunT11  28885  uunT11p1  28886  uunT11p2  28887  uunT12  28888  uunT12p1  28889  uunT12p2  28890  uunT12p3  28891  uunT12p4  28892  uunT12p5  28893  uun111  28894  3anidm12p2  28896  uun123  28897  3impdirp1  28905  undif3VD  28974  a9e2ndeqVD  29001  2uasbanhVD  29003  a9e2ndeqALT  29024  bnj945  29121  bnj1379  29179  bnj1459  29191  bnj557  29249  bnj571  29254  bnj849  29273  bnj964  29291  bnj978  29297  bnj1018  29310  bnj1020  29311  bnj1033  29315  bnj1175  29350  bnj1398  29380  bnj1417  29387  bnj1523  29417  sbi2NEW7  29539  sb5rfNEW7  29563  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