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

Theorem sylbir 205
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 198 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3i  257  ex  424  3ori  1244  19.38  1802  equsex  1957  ax12olem3  1962  ax12olem5OLD  1969  sbi2  2097  sb5rf  2123  ax11eq  2227  ax11el  2228  mo  2260  mo2  2267  2mo  2316  axie2  2363  bm1.1  2372  necon1i  2594  sbhypf  2944  vtocl2  2950  vtocl3  2951  reu6  3066  uneqin  3535  inelcm  3625  difin0ss  3637  difprsn1  3878  tppreqb  3882  unissint  4016  intminss  4018  iununi  4116  bm1.3ii  4274  moabex  4363  copsex2g  4385  opelopabt  4408  eusv2nf  4661  reusv3i  4670  reuxfr2d  4686  onminesb  4718  onminsb  4719  onintrab  4721  onnminsb  4724  onsucuni2  4754  tfindsg2  4781  eqrelrel  4917  opeliunxp2  4953  opelrn  5041  issref  5187  ssxpb  5243  xpima  5253  dmsn0el  5279  relcoi2  5337  iotanul  5373  dffv2  5735  fnfvrnss  5835  fressnfv  5859  fconst5  5888  fconstfv  5893  zfrep6  5907  f1mpt  5946  isocnv3  5991  f1owe  6012  ovprc  6047  fo1stres  6309  fo2ndres  6310  bropopvvv  6365  frxp  6392  mpt2xopoveqd  6408  reldmtpos  6423  tfrlem5  6577  tfrlem9  6582  tfr2  6595  rdgsuc  6618  oaordi  6725  oeordi  6766  omopthi  6836  fvmptmap  6986  mptelixpg  7035  ener  7090  domtr  7096  snfi  7123  unen  7125  xpf1o  7205  mapen  7207  unxpdomlem3  7251  isinf  7258  frfi  7288  unblem1  7295  unfi  7310  fofinf1o  7323  inf3lem2  7517  inf3lem5  7520  cantnfreslem  7564  cantnfp1lem1  7567  cantnfp1lem3  7569  tcmin  7613  r1ordg  7637  r1ord  7639  rankr1ai  7657  r1val3  7697  bndrank  7700  unbndrank  7701  rankr1b  7723  rankxplim3  7738  tcrank  7741  xpnum  7771  cardmin2  7818  infxpenlem  7828  fseqen  7841  dfac8clem  7846  alephsson  7914  alephfp  7922  dfac4  7936  kmlem6  7968  kmlem8  7970  kmlem9  7971  infpssr  8121  fin1a2lem12  8224  axcc4  8252  axcc4dom  8254  ac6s2  8299  zornn0g  8318  cardidg  8356  unsnen  8361  pwcfsdom  8391  cfpwsdom  8392  gchpwdom  8482  r1tskina  8590  intgru  8622  indpi  8717  nqereu  8739  supsrlem  8919  letrii  9130  infmrcl  9919  dfnn3  9946  zaddcl  10249  uzindOLD  10296  nn0ind  10298  fnn0ind  10301  ublbneg  10492  fzo0end  11115  elfznelfzo  11119  fzind2  11125  injresinjlem  11126  faclbnd4lem1  11511  hashinf  11550  hasheqf1oi  11562  hashgt0elex  11597  hash2prde  11615  hashfacen  11630  rediv  11863  imdiv  11870  sqr0  11974  fsump1i  12480  cos1bnd  12715  sinltx  12717  rpnnen2lem1  12741  rpnnen2lem2  12742  rpnnen2  12752  odd2np1  12835  gcdcllem1  12938  gcdaddmlem  12955  algfx  12998  odzval  13104  odzdvds  13108  opoe  13112  omoe  13113  opeo  13114  omeo  13115  prmreclem5  13215  mul4sq  13249  imasaddfnlem  13680  mreexexlem4d  13799  lubval  14363  glbval  14368  joinlem  14374  meetlem  14381  clatlem  14466  gictr  14989  cntzval  15047  efgsfo  15298  efgrelexlemb  15309  dprd2da  15527  lssacs  15970  cnfldinv  16655  ocvval  16817  eltopspOLD  16906  tpsexOLD  16907  opnnei  17107  ordtbas2  17177  ordtrest2lem  17189  lmmo  17366  fincmp  17378  txbas  17520  ptcnplem  17574  tx2ndc  17604  hmphtr  17736  fbun  17793  filcon  17836  ptcmplem5  18008  cnextcn  18019  utoptop  18185  restutopopn  18189  ucncn  18236  metust  18478  cfilucfil  18479  elcncf1di  18796  xrhmeo  18842  phtpycc  18887  copco  18914  pcohtpylem  18915  pcopt  18918  pcopt2  18919  ovolval  19237  iunmbl2  19318  itg2splitlem  19507  cpnfval  19685  plyval  19979  fta1  20092  aaliou2b  20125  ulmdvlem3  20185  radcnvlem2  20197  dvradcnv  20204  reeff1o  20230  sincosq1lem  20272  sincosq2sgn  20274  sincosq4sgn  20276  sinq12ge0  20283  logrncl  20332  eflog  20341  cxpge0  20441  atanf  20587  atanbnd  20633  lgsne0  20984  mul2sq  21016  pntibnd  21154  ostth  21200  isusgra0  21243  usgraedg4  21272  nbgranself2  21314  wlkntrllem5  21417  wlkdvspth  21456  cyclnspth  21466  3v3e3cycl2  21499  3v3e3cycl  21500  4cycl4dv  21502  vdgrf  21517  eupath2lem1  21547  isgrpo  21632  ismgm  21756  isrngo  21814  rngoablo2  21858  rngoueqz  21866  isdivrngo  21867  vci  21875  vcex  21907  nmogtmnf  22119  siilem1  22200  siii  22202  ajmoi  22208  bcsiALT  22529  hhcms  22553  ocval  22630  hsupval  22684  omlsilem  22752  h1de2bi  22904  h1de2ctlem  22905  hosubeq0i  23177  adjmo  23183  nmopgtmnf  23219  nlfnval  23232  nmcopex  23380  nmcfnex  23404  riesz4i  23414  riesz1  23416  riesz2  23417  opsqrlem1  23491  superpos  23705  hatomistici  23713  chpssati  23714  mdsymlem3  23756  mdsymi  23762  3o1cs  23801  3o2cs  23802  3o3cs  23803  qqhval2  24165  logb1  24199  esumfsup  24256  esumcvg  24272  cntnevol  24376  dya2icoseg2  24422  dya2iocnei  24426  cndprobprob  24475  ballotlemsdom  24548  ballotth  24574  igamf  24614  igamcl  24615  txpcon  24698  ghomgrp  24880  setinds  25158  dfon2lem7  25169  dfon2lem8  25170  nnsinds  25241  nn0sinds  25242  poseq  25277  soseq  25278  wfrlem4  25283  wfrlem12  25291  wfrlem16  25295  wfr2  25297  tfrALTlem  25300  frrlem4  25308  frrlem11  25317  nodenselem4  25362  nocvxminlem  25368  nocvxmin  25369  pprodss4v  25448  fullfunfv  25510  altxpsspw  25536  mptelee  25548  axlowdimlem9  25603  axlowdimlem12  25606  axcontlem2  25618  axcontlem12  25628  funtransport  25679  fvtransport  25680  funray  25788  fvray  25789  funline  25790  fvline  25792  bpolydiflem  25814  bpoly3  25818  bpoly4  25819  bisym1  25883  onsucconi  25901  onsucsuccmpi  25907  itg2addnclem  25957  finminlem  26012  sdclem2  26137  totbndbnd  26189  exidresid  26245  isdrngo1  26263  isdrngo2  26265  ispridl2  26339  prtlem11  26406  mptfcl  26468  fphpd  26568  elmnc  27010  itgoval  27035  pm11.71  27265  iotavalsb  27302  sbiota1  27303  stoweidlem3  27420  stoweidlem17  27434  rexrsb  27615  raaan2  27621  afv0nbfvbi  27684  afvfv0bi  27685  afveu  27686  fnbrafvb  27687  afvres  27705  tz6.12-afv  27706  dmfcoafv  27708  afvco2  27709  aovprc  27721  aovrcl  27722  aovmpt4g  27734  frgra2v  27752  frgra3vlem1  27753  frgra3vlem2  27754  frgrancvvdeqlem2  27783  frgrancvvdeqlem3  27784  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  frgrawopreglem5  27800  secval  27836  cscval  27837  cotval  27838  2uasbanh  27991  eel0TT  28148  eelT00  28149  eelTTT  28150  eelT11  28152  eelT12  28156  eelTT1  28158  eelT01  28159  eel0T1  28160  eelTT  28224  uunT1p1  28234  uun121  28236  uun121p1  28237  un2122  28243  uunTT1  28246  uunTT1p1  28247  uunTT1p2  28248  uunT11  28249  uunT11p1  28250  uunT11p2  28251  uunT12  28252  uunT12p1  28253  uunT12p2  28254  uunT12p3  28255  uunT12p4  28256  uunT12p5  28257  uun111  28258  3anidm12p2  28260  uun123  28261  3impdirp1  28269  undif3VD  28335  a9e2ndeqVD  28362  2uasbanhVD  28364  a9e2ndeqALT  28385  bnj945  28482  bnj1379  28540  bnj1459  28552  bnj557  28610  bnj571  28615  bnj849  28634  bnj964  28652  bnj978  28658  bnj1018  28671  bnj1020  28672  bnj1033  28676  bnj1175  28711  bnj1398  28741  bnj1417  28748  bnj1523  28778  sbi2NEW7  28900  sb5rfNEW7  28924  lkr0f  29209  hl2at  29519  dalemswapyz  29770  pclfinclN  30064  osumcllem11N  30080  pexmidlem8N  30091  ltrnnid  30250
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 178
  Copyright terms: Public domain W3C validator