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

Theorem syl5bb 250
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1  |-  ( ph  <->  ps )
syl5bb.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bb  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3  |-  ( ph  <->  ps )
21a1i 12 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 246 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  syl5rbb  251  syl5bbr  252  3bitr4g  281  imim21b  358  cad0  1396  had1  1398  ax12olem27  1661  sbcom  1983  abbi  2359  necon3abid  2445  necon3bid  2447  necon1abid  2465  r19.21t  2590  ceqsralt  2749  ceqsrexv  2838  ceqsrex2v  2840  elab2g  2853  elrabf  2859  eueq2  2876  eqreu  2896  reu8  2900  ru  2920  sbcralt  2993  sbcabel  2998  csbnestgf  3057  disjpss  3412  ralprg  3586  rexprg  3587  difsn  3657  opthpr  3690  ralunsn  3715  dfiin2g  3834  iunxsng  3878  elpwuni  3887  disjxun  3918  opelopabt  4170  opelopabga  4171  brabga  4172  dfid3  4203  frirr  4263  wereu2  4283  ordtri4  4322  oneqmini  4336  elsucg  4352  elsuc2g  4353  dfwe2  4464  ssonprc  4474  ordpwsuc  4497  dfom2  4549  brab2a  4645  opeliunxp  4647  posn  4665  sosn  4666  frsn  4667  brab2ga  4670  opbrop  4674  elrnmpt1  4835  elrnmptg  4836  eliniseg2  4960  poleloe  4984  cnvpo  5119  dffun8  5139  fncnv  5171  fununi  5173  fnssresb  5213  fnimaeq0  5222  funcocnv2  5355  dffn5  5420  funimass4  5425  fnsnfv  5434  dmfco  5445  fndmdif  5481  fvimacnvi  5491  fvimacnvALT  5496  unpreima  5503  respreima  5506  fmptco  5543  fressnfv  5559  fnsuppres  5584  elunirnALT  5631  dff13  5635  fliftel  5660  isoini  5687  f1oiso  5700  f1oweALT  5703  eloprabga  5786  resoprab2  5793  ralrnmpt2  5810  ovid  5816  ov  5819  ovg  5838  ofrfval2  5948  fmpt2x  6042  ovmptss  6052  1stconst  6059  2ndconst  6060  brtpos2  6092  pwnss  6183  dfsmo2  6250  tfrlem1  6277  rdglim2  6331  seqomlem2  6349  omeu  6469  oeeui  6486  brdifun  6573  eqerlem  6578  brecop  6637  erovlem  6640  eceqoveq  6649  mapsn  6695  mptelixpg  6739  map1  6824  xpsnen  6831  xpdom2  6842  omxpenlem  6848  xpf1o  6908  mapunen  6915  onfin  6936  fimaxg  6989  fodomfib  7021  fofinf1o  7022  fipreima  7045  supub  7094  ordtypecbv  7116  ordtypelem3  7119  ordtypelem9  7125  hartogslem1  7141  wofib  7144  wemapso2lem  7149  wemapso2  7151  noinfep  7244  noinfepOLD  7245  cantnf  7279  rankbnd2  7425  domtri2  7506  infxpenc2  7533  fseqdom  7537  acni2  7557  dfac9  7646  cfeq0  7766  cfsuc  7767  cflim3  7772  cfslb  7776  cofsmo  7779  enfin2i  7831  isfin3ds  7839  isf33lem  7876  fin1a2lem5  7914  axdc2lem  7958  zorn2g  8014  fodomb  8035  brdom7disj  8040  brdom6disj  8041  iundom2g  8046  cfpwsdom  8086  elgch  8124  fpwwe2cbv  8132  fpwwecbv  8146  pwfseqlem3  8162  pwfseqlem4a  8163  pwfseqlem4  8164  ltpiord  8391  nlt1pi  8410  nqereu  8433  addclprlem1  8520  1idpr  8533  reclem3pr  8553  ltsosr  8596  map2psrpr  8612  supsrlem  8613  axrrecex  8665  xrlenlt  8770  addsubeq4  8946  renegcli  8988  lesub0  9170  wloglei  9185  conjmul  9357  rereccl  9358  infm3  9593  supmul1  9599  supmullem1  9600  supmullem2  9601  supmul  9602  creui  9621  nndiv  9666  elznn0  9917  prime  9971  eqreznegel  10182  zsupss  10186  rebtwnz  10194  ltxr  10336  elixx3g  10547  ixxun  10550  ioo0  10559  ico0  10580  ioc0  10581  icc0  10582  difreicc  10645  iccf1o  10656  elfz2  10667  fzn  10688  fznn  10730  fzshftral  10747  fzosplitsni  10799  om2uzisoi  10895  sq11i  11072  hashsdom  11241  wrdval  11293  cjreb  11485  rexfiuz  11708  cau3lem  11715  rlim2  11847  ello12  11867  ello1mpt  11872  elo12  11878  o1lo1  11888  lo1resb  11915  o1resb  11917  o1compt  11938  caucvgb  12029  mertens  12216  ruclem12  12393  divides  12407  odd2np1  12461  oddm1even  12462  sadadd2lem2  12515  gcdcllem2  12565  bezoutlem2  12592  bezoutlem3  12593  bezoutlem4  12594  isprm2  12640  isprm3  12641  prmreclem2  12838  prmreclem5  12841  prmreclem6  12842  4sqlem2  12870  4sqlem12  12877  vdwmc  12899  vdwpc  12901  vdwlem6  12907  vdwlem10  12911  vdwnn  12919  ramval  12929  0ram  12941  prdsleval  13250  pwsle  13265  imasleval  13317  xpsfrnel2  13341  xpsle  13357  isacs2  13400  mreacs  13404  acsfn  13405  iscatd2  13427  catpropd  13456  isssc  13541  evlfcl  13840  uncfcurf  13857  pltval  13938  lubid  13960  tosso  13986  oduleg  14080  oduclatb  14092  isipodrs  14108  odudlatb  14134  spwpr2  14172  spwex  14173  gsumvalx  14286  grplmulf1o  14377  grplactcnv  14399  elnmz  14491  eqgid  14504  isghm  14518  ghmeqker  14544  resscntz  14642  odmulgeq  14705  sylow3lem3  14775  sylow3lem6  14778  efgval2  14868  efgsdm  14874  efgrelexlema  14893  efgcpbllemb  14899  iscyggen2  15003  cyggenod  15006  eldprd  15074  dprdf11  15093  dprddisj2  15109  pgpfac1lem2  15145  pgpfac1  15150  drngid2  15363  issubrg  15380  islmod  15466  aspval2  15918  psrbag  15944  zndvds  16335  znleval  16340  iunocv  16413  pjfval2  16441  pjdm2  16443  istopg  16473  istpsOLD  16490  basgen2  16559  isclo  16656  mretopd  16661  isnei  16672  isperf3  16716  restdis  16741  restcls  16743  restlp  16745  restperf  16746  iscn  16797  iscnp  16799  lmbr2  16821  lmbrf  16822  ordtt1  16939  cmpsub  16959  hauscmplem  16965  cmpfi  16967  dfcon2  16977  1stcelcls  17019  1stccn  17021  nllyi  17033  subislly  17039  elkgen  17063  ptpjpre1  17098  ptuni2  17103  ptclsg  17141  ptcnplem  17147  txcn  17152  hausdiag  17171  txhaus  17173  txkgen  17178  xkoptsub  17180  cnmpt21  17197  elqtop  17220  tgqtop  17235  r0cld  17261  elfg  17398  fbasrn  17411  trfil2  17414  trfil3  17415  fin1aufil  17459  elfm2  17475  elfm3  17477  flimopn  17502  fbflim  17503  flfnei  17518  flftg  17523  cnpflf2  17527  txflf  17533  fclsbas  17548  alexsubALTlem4  17576  snclseqg  17630  tgphaus  17631  tsmsfbas  17642  tsmssubm  17657  prdsxmetlem  17764  imasdsf1olem  17769  xpsdsval  17777  blres  17809  isxms2  17826  metcnp  17919  txmetcnp  17925  txmetcn  17926  dscopn  17928  isngp4  17965  cnblcld  18116  metnrmlem1a  18194  icoopnst  18269  iocopnst  18270  elpi1  18375  lmmbr2  18517  cfil3i  18527  caucfil  18541  iscmet3  18551  lmclim  18560  metcld2  18564  bcthlem4  18581  minveclem3b  18624  minveclem6  18630  minveclem7  18631  ivthle  18648  ivthle2  18649  evthicc2  18652  ovolfioo  18659  ovolficc  18660  ovolgelb  18671  dyadmax  18785  subopnmbl  18791  ismbf3d  18841  mbfimaopnlem  18842  mbfimaopn2  18844  mbfaddlem  18847  mbfsup  18851  mbfinf  18852  i1f1lem  18876  i1fmulclem  18889  itg1climres  18901  mbfi1fseqlem4  18905  itg2monolem1  18937  itg2gt0  18947  isibl  18952  iblcnlem1  18974  ellimc2  19059  dvcnvrelem1  19196  itgsubst  19228  mdegleb  19282  fta1glem2  19384  quotval  19504  vieta1lem1  19522  vieta1lem2  19523  ulm2  19596  ulmcaulem  19603  ulmcau  19604  radcnvlt1  19626  sineq0  19721  cos11  19727  recosf1o  19729  efopn  19837  cxpeq  19965  mcubic  19975  birthdaylem3  20080  rlimcnp  20092  xrlimcnp  20095  wilth  20141  isppw  20184  isppw2  20185  mumullem2  20250  sqff1o  20252  dvdsmulf1o  20266  fsumvma  20284  fsumvma2  20285  vmasum  20287  chpchtsum  20290  lgsne0  20404  lgseisenlem2  20421  lgsquadlem1  20425  lgsquadlem2  20426  dchrmusumlema  20474  rpvmasum2  20493  dchrisum0lema  20495  pntibndlem3  20573  pntlemi  20585  pntleml  20592  pnt3  20593  grpodiveq  20753  opidon  20819  issmgrp  20831  ismndo  20840  isrngo  20875  isdivrngo  20928  isvclem  20963  isnvlem  20996  isphg  21225  isph  21230  phoeqi  21266  ubthlem3  21281  minvecolem5  21290  minvecolem6  21291  minvecolem7  21292  hhph  21587  issh3  21629  nmopub  22318  nmfnleub  22335  adjeq  22345  adjvalval  22347  elunop2  22423  lnophm  22429  nmcexi  22436  cnlnadjlem5  22481  cnlnadjeui  22487  adjbd1o  22495  jpi  22680  mddmd2  22719  chrelati  22774  chrelat2i  22775  cvexchlem  22778  dmdbr5ati  22832  cdjreui  22842  cdj3i  22851  eldmgm  22865  dmgmaddn0  22866  subfacp1lem3  22884  subfacp1lem6  22887  subfacp1  22888  txpcon  22934  sconpi1  22941  rescon  22948  cvmscbv  22960  cvmsval  22968  cvmlift2lem13  23017  cvmlift3lem2  23022  cvmlift3  23030  eupath2  23075  divelunit  23250  br8  23283  br6  23284  br4  23285  distel  23328  elpred  23345  poseq  23421  axsltsolem1  23489  axfelem20  23533  imageval  23643  dfrdg4  23662  altopthg  23675  altopthbg  23676  brbtwn  23701  brcgr  23702  brbtwn2  23707  colinearalg  23712  axeuclidlem  23764  axcontlem2  23767  axcontlem4  23769  axcontlem7  23772  brcolinear2  23855  lineext  23873  brsegle  23905  seglelin  23913  broutsideof2  23919  bpolyval  23958  onsuct0  24054  fnovpop  24203  twsymr  24243  prj1b  24244  prj3  24245  inttpemp  24305  repcpwti  24327  vecval1b  24617  svs2  24653  fgsb2  24721  islimrs3  24747  islimrs4  24748  bwt2  24758  supnuf  24795  supexr  24797  tcnvec  24856  ismgra  24876  isalg  24887  isded  24902  iscatOLD  24920  dualcat2  24950  issrc  25033  vtarsuelt  25061  sgplpte21a  25299  isibcg  25357  isfne4  25435  isfne2  25437  isfne3  25438  fneval  25453  topfneec  25457  neibastop2lem  25475  neibastop2  25476  neifg  25486  filnetlem4  25496  fdc  25621  heibor1  25700  rrncmslem  25722  rrnheibor  25727  isfldidl2  25860  isdmn3  25865  prtlem13  25902  prter3  25916  fnnfpeq0  25924  ralxpxfr2d  25926  ellz1  26012  lzunuz  26013  fz1eqin  26014  diophrex  26021  rexrabdioph  26041  rexfrabdioph  26042  2rexfrabdioph  26043  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  fzneg  26235  expdioph  26282  wepwsolem  26304  fnwe2lem2  26314  islmodfg  26333  kercvrlsm  26347  dsmmelbas  26371  ellspd  26420  islindf  26448  islindf4  26474  f1omvdconj  26555  sdrgacs  26675  pm10.52  26726  iotasbc  26786  pm14.122a  26789  pm14.122b  26790  pm14.123a  26792  rusbcALT  26806  fvsb  26822  gte-lte  26883  gt-lt  26884  bnj976  27498  bnj944  27659  bnj1173  27721  bnj1321  27746  bnj1373  27749  bnj1417  27760  lrelat  27893  islshpat  27896  lshpsmreu  27988  lkrpssN  28042  cmtvalN  28090  omllaw2N  28123  cvrval  28148  cvrval2  28153  cvlsupr3  28223  3dim0  28335  islln2  28389  islpln5  28413  islpln2  28414  islpln2ah  28427  islvol5  28457  islvol2  28458  4atlem11  28487  pmapglbx  28647  cdleme18d  29173  cdlemefrs29bpre0  29274  cdlemb3  29484  cdlemg33b  29585  dvhb1dimN  29864  dia11N  29927  cdlemm10N  29997  dib11N  30039  dib1dim  30044  dibglbN  30045  diblsmopel  30050  dihopelvalcpre  30127  dih11  30144  dihmeetlem4preN  30185  dihmeetlem13N  30198  lcfrvalsnN  30420  lcfrlem9  30429  lcf1o  30430  mapdval4N  30511  baerlem3lem2  30589  baerlem5alem2  30590  baerlem5blem2  30591  hdmap1fval  30676  hdmapfval  30709  hdmapglem7a  30809  hlhillcs  30840
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator