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  1984  abbi  2366  necon3abid  2452  necon3bid  2454  necon1abid  2472  r19.21t  2599  ceqsralt  2762  ceqsrexv  2852  ceqsrex2v  2854  elab2g  2867  elrabf  2873  eueq2  2890  eqreu  2910  reu8  2914  ru  2934  sbcralt  3007  sbcabel  3012  csbnestgf  3071  disjpss  3447  ralprg  3623  rexprg  3624  difsn  3696  opthpr  3731  ralunsn  3756  dfiin2g  3877  iunxsng  3921  elpwuni  3930  disjxun  3961  opelopabt  4214  opelopabga  4215  brabga  4216  dfid3  4247  frirr  4307  wereu2  4327  ordtri4  4366  oneqmini  4380  elsucg  4396  elsuc2g  4397  dfwe2  4510  ssonprc  4520  ordpwsuc  4543  dfom2  4595  brab2a  4691  opeliunxp  4693  posn  4711  sosn  4712  frsn  4713  brab2ga  4716  opbrop  4720  elrnmpt1  4881  elrnmptg  4882  eliniseg2  5006  poleloe  5030  cnvpo  5165  dffun8  5185  fncnv  5217  fununi  5219  fnssresb  5259  fnimaeq0  5268  funcocnv2  5401  dffn5  5467  funimass4  5472  fnsnfv  5481  dmfco  5492  fndmdif  5528  fvimacnvi  5538  fvimacnvALT  5543  unpreima  5550  respreima  5553  fmptco  5590  fressnfv  5606  fnsuppres  5631  elunirnALT  5678  dff13  5682  fliftel  5707  isoini  5734  f1oiso  5747  f1oweALT  5750  eloprabga  5833  resoprab2  5840  ralrnmpt2  5857  ovid  5863  ov  5866  ovg  5885  ofrfval2  5995  fmpt2x  6089  ovmptss  6099  1stconst  6106  2ndconst  6107  brtpos2  6139  pwnss  6230  dfsmo2  6297  tfrlem1  6324  rdglim2  6378  seqomlem2  6396  omeu  6516  oeeui  6533  brdifun  6620  eqerlem  6625  brecop  6684  erovlem  6687  eceqoveq  6696  mapsn  6742  mptelixpg  6786  map1  6872  xpsnen  6879  xpdom2  6890  omxpenlem  6896  xpf1o  6956  mapunen  6963  onfin  6984  fimaxg  7037  fodomfib  7069  fofinf1o  7070  fipreima  7094  supub  7143  ordtypecbv  7165  ordtypelem3  7168  ordtypelem9  7174  hartogslem1  7190  wofib  7193  wemapso2lem  7198  wemapso2  7200  noinfep  7293  noinfepOLD  7294  cantnf  7328  rankbnd2  7474  domtri2  7555  infxpenc2  7582  fseqdom  7586  acni2  7606  dfac9  7695  cfeq0  7815  cfsuc  7816  cflim3  7821  cfslb  7825  cofsmo  7828  enfin2i  7880  isfin3ds  7888  isf33lem  7925  fin1a2lem5  7963  axdc2lem  8007  zorn2g  8063  fodomb  8084  brdom7disj  8089  brdom6disj  8090  iundom2g  8095  cfpwsdom  8139  elgch  8177  fpwwe2cbv  8185  fpwwecbv  8199  pwfseqlem3  8215  pwfseqlem4a  8216  pwfseqlem4  8217  ltpiord  8444  nlt1pi  8463  nqereu  8486  addclprlem1  8573  1idpr  8586  reclem3pr  8606  ltsosr  8649  map2psrpr  8665  supsrlem  8666  axrrecex  8718  xrlenlt  8823  addsubeq4  8999  renegcli  9041  lesub0  9223  wloglei  9238  conjmul  9410  rereccl  9411  infm3  9646  supmul1  9652  supmullem1  9653  supmullem2  9654  supmul  9655  creui  9674  nndiv  9719  elznn0  9970  prime  10024  eqreznegel  10235  zsupss  10239  rebtwnz  10247  ltxr  10389  elixx3g  10600  ixxun  10603  ioo0  10612  ico0  10633  ioc0  10634  icc0  10635  difreicc  10698  iccf1o  10709  elfz2  10720  fzn  10741  fznn  10783  fzshftral  10800  fzosplitsni  10852  om2uzisoi  10948  sq11i  11125  hashsdom  11294  wrdval  11346  cjreb  11538  rexfiuz  11761  cau3lem  11768  rlim2  11900  ello12  11920  ello1mpt  11925  elo12  11931  o1lo1  11941  lo1resb  11968  o1resb  11970  o1compt  11991  caucvgb  12082  mertens  12269  ruclem12  12446  divides  12460  odd2np1  12514  oddm1even  12515  sadadd2lem2  12568  gcdcllem2  12618  bezoutlem2  12645  bezoutlem3  12646  bezoutlem4  12647  isprm2  12693  isprm3  12694  prmreclem2  12891  prmreclem5  12894  prmreclem6  12895  4sqlem2  12923  4sqlem12  12930  vdwmc  12952  vdwpc  12954  vdwlem6  12960  vdwlem10  12964  vdwnn  12972  ramval  12982  0ram  12994  prdsleval  13303  pwsle  13318  imasleval  13370  xpsfrnel2  13394  xpsle  13410  isacs2  13482  mreacs  13487  acsfn  13488  iscatd2  13510  catpropd  13539  isssc  13624  evlfcl  13923  uncfcurf  13940  pltval  14021  lubid  14043  tosso  14069  oduleg  14163  oduclatb  14175  isipodrs  14191  odudlatb  14226  spwpr2  14264  spwex  14265  gsumvalx  14378  grplmulf1o  14469  grplactcnv  14491  elnmz  14583  eqgid  14596  isghm  14610  ghmeqker  14636  resscntz  14734  odmulgeq  14797  sylow3lem3  14867  sylow3lem6  14870  efgval2  14960  efgsdm  14966  efgrelexlema  14985  efgcpbllemb  14991  iscyggen2  15095  cyggenod  15098  eldprd  15166  dprdf11  15185  dprddisj2  15201  pgpfac1lem2  15237  pgpfac1  15242  drngid2  15455  issubrg  15472  islmod  15558  aspval2  16013  psrbag  16039  zndvds  16430  znleval  16435  iunocv  16508  pjfval2  16536  pjdm2  16538  istopg  16568  istpsOLD  16585  basgen2  16654  isclo  16751  mretopd  16756  isnei  16767  isperf3  16811  restdis  16836  restcls  16838  restlp  16840  restperf  16841  iscn  16892  iscnp  16894  lmbr2  16916  lmbrf  16917  ordtt1  17034  cmpsub  17054  hauscmplem  17060  cmpfi  17062  dfcon2  17072  1stcelcls  17114  1stccn  17116  nllyi  17128  subislly  17134  elkgen  17158  ptpjpre1  17193  ptuni2  17198  ptclsg  17236  ptcnplem  17242  txcn  17247  hausdiag  17266  txhaus  17268  txkgen  17273  xkoptsub  17275  cnmpt21  17292  elqtop  17315  tgqtop  17330  r0cld  17356  elfg  17493  fbasrn  17506  trfil2  17509  trfil3  17510  fin1aufil  17554  elfm2  17570  elfm3  17572  flimopn  17597  fbflim  17598  flfnei  17613  flftg  17618  cnpflf2  17622  txflf  17628  fclsbas  17643  alexsubALTlem4  17671  snclseqg  17725  tgphaus  17726  tsmsfbas  17737  tsmssubm  17752  prdsxmetlem  17859  imasdsf1olem  17864  xpsdsval  17872  blres  17904  isxms2  17921  metcnp  18014  txmetcnp  18020  txmetcn  18021  dscopn  18023  isngp4  18060  cnblcld  18211  metnrmlem1a  18289  icoopnst  18364  iocopnst  18365  elpi1  18470  lmmbr2  18612  cfil3i  18622  caucfil  18636  iscmet3  18646  lmclim  18655  metcld2  18659  bcthlem4  18676  minveclem3b  18719  minveclem6  18725  minveclem7  18726  ivthle  18743  ivthle2  18744  evthicc2  18747  ovolfioo  18754  ovolficc  18755  ovolgelb  18766  dyadmax  18880  subopnmbl  18886  ismbf3d  18936  mbfimaopnlem  18937  mbfimaopn2  18939  mbfaddlem  18942  mbfsup  18946  mbfinf  18947  i1f1lem  18971  i1fmulclem  18984  itg1climres  18996  mbfi1fseqlem4  19000  itg2monolem1  19032  itg2gt0  19042  isibl  19047  iblcnlem1  19069  ellimc2  19154  dvcnvrelem1  19291  itgsubst  19323  mdegleb  19377  fta1glem2  19479  quotval  19599  vieta1lem1  19617  vieta1lem2  19618  ulm2  19691  ulmcaulem  19698  ulmcau  19699  radcnvlt1  19721  sineq0  19816  cos11  19822  recosf1o  19824  efopn  19932  cxpeq  20024  mcubic  20070  birthdaylem3  20175  rlimcnp  20187  xrlimcnp  20190  wilth  20236  isppw  20279  isppw2  20280  mumullem2  20345  sqff1o  20347  dvdsmulf1o  20361  fsumvma  20379  fsumvma2  20380  vmasum  20382  chpchtsum  20385  lgsne0  20499  lgseisenlem2  20516  lgsquadlem1  20520  lgsquadlem2  20521  dchrmusumlema  20569  rpvmasum2  20588  dchrisum0lema  20590  pntibndlem3  20668  pntlemi  20680  pntleml  20687  pnt3  20688  grpodiveq  20848  opidon  20914  issmgrp  20926  ismndo  20935  isrngo  20970  isdivrngo  21023  isvclem  21058  isnvlem  21091  isphg  21320  isph  21325  phoeqi  21361  ubthlem3  21376  minvecolem5  21385  minvecolem6  21386  minvecolem7  21387  hhph  21682  issh3  21724  nmopub  22413  nmfnleub  22430  adjeq  22440  adjvalval  22442  elunop2  22518  lnophm  22524  nmcexi  22531  cnlnadjlem5  22576  cnlnadjeui  22582  adjbd1o  22590  jpi  22775  mddmd2  22814  chrelati  22869  chrelat2i  22870  cvexchlem  22873  dmdbr5ati  22927  cdjreui  22937  cdj3i  22946  ballotlemfmpn  22979  eldmgm  23031  dmgmaddn0  23032  subfacp1lem3  23050  subfacp1lem6  23053  subfacp1  23054  txpcon  23100  sconpi1  23107  rescon  23114  cvmscbv  23126  cvmsval  23134  cvmlift2lem13  23183  cvmlift3lem2  23188  cvmlift3  23196  eupath2  23241  divelunit  23416  br8  23449  br6  23450  br4  23451  distel  23494  elpred  23511  poseq  23587  axsltsolem1  23655  axfelem20  23699  imageval  23809  dfrdg4  23828  altopthg  23841  altopthbg  23842  brbtwn  23867  brcgr  23868  brbtwn2  23873  colinearalg  23878  axeuclidlem  23930  axcontlem2  23933  axcontlem4  23935  axcontlem7  23938  brcolinear2  24021  lineext  24039  brsegle  24071  seglelin  24079  broutsideof2  24085  bpolyval  24124  onsuct0  24220  fnovpop  24369  twsymr  24409  prj1b  24410  prj3  24411  inttpemp  24471  repcpwti  24493  vecval1b  24783  svs2  24819  fgsb2  24887  islimrs3  24913  islimrs4  24914  bwt2  24924  supnuf  24961  supexr  24963  tcnvec  25022  ismgra  25042  isalg  25053  isded  25068  iscatOLD  25086  dualcat2  25116  issrc  25199  vtarsuelt  25227  sgplpte21a  25465  isibcg  25523  isfne4  25601  isfne2  25603  isfne3  25604  fneval  25619  topfneec  25623  neibastop2lem  25641  neibastop2  25642  neifg  25652  filnetlem4  25662  fdc  25787  heibor1  25866  rrncmslem  25888  rrnheibor  25893  isfldidl2  26026  isdmn3  26031  prtlem13  26068  prter3  26082  fnnfpeq0  26090  ralxpxfr2d  26092  ellz1  26178  lzunuz  26179  fz1eqin  26180  diophrex  26187  rexrabdioph  26207  rexfrabdioph  26208  2rexfrabdioph  26209  3rexfrabdioph  26210  4rexfrabdioph  26211  6rexfrabdioph  26212  7rexfrabdioph  26213  fzneg  26401  expdioph  26448  wepwsolem  26470  fnwe2lem2  26480  islmodfg  26499  kercvrlsm  26513  dsmmelbas  26537  ellspd  26586  islindf  26614  islindf4  26640  f1omvdconj  26721  sdrgacs  26841  pm10.52  26892  iotasbc  26952  pm14.122a  26955  pm14.122b  26956  pm14.123a  26958  rusbcALT  26972  fvsb  26988  stoweidlem34  27083  gte-lte  27206  gt-lt  27207  bnj976  27821  bnj944  27982  bnj1173  28044  bnj1321  28069  bnj1373  28072  bnj1417  28083  ax11wdemoK  28155  ax12olem27X  28212  lrelat  28334  islshpat  28337  lshpsmreu  28429  lkrpssN  28483  cmtvalN  28531  omllaw2N  28564  cvrval  28589  cvrval2  28594  cvlsupr3  28664  3dim0  28776  islln2  28830  islpln5  28854  islpln2  28855  islpln2ah  28868  islvol5  28898  islvol2  28899  4atlem11  28928  pmapglbx  29088  cdleme18d  29614  cdlemefrs29bpre0  29715  cdlemb3  29925  cdlemg33b  30026  dvhb1dimN  30305  dia11N  30368  cdlemm10N  30438  dib11N  30480  dib1dim  30485  dibglbN  30486  diblsmopel  30491  dihopelvalcpre  30568  dih11  30585  dihmeetlem4preN  30626  dihmeetlem13N  30639  lcfrvalsnN  30861  lcfrlem9  30870  lcf1o  30871  mapdval4N  30952  baerlem3lem2  31030  baerlem5alem2  31031  baerlem5blem2  31032  hdmap1fval  31117  hdmapfval  31150  hdmapglem7a  31250  hlhillcs  31281
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