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

Theorem syl5bb 249
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 11 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 245 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5rbb  250  syl5bbr  251  3bitr4g  280  imim21b  357  cad0  1406  had1  1408  ax11wdemo  1730  ax12olem6OLD  1975  sbcom  2124  abbi  2499  necon3abid  2585  necon3bid  2587  necon1abid  2605  r19.21t  2736  ceqsralt  2924  ceqsrexv  3014  ceqsrex2v  3016  elab2g  3029  elrabf  3036  eueq2  3053  eqreu  3071  reu8  3075  ru  3105  sbcralt  3178  csbnestgf  3244  disjpss  3623  ralprg  3802  rexprg  3803  difsn  3878  opthpr  3920  ralunsn  3947  dfiin2g  4068  iunxsng  4112  elpwuni  4121  disjxun  4153  pwnss  4308  opelopabt  4410  opelopabga  4411  brabga  4412  dfid3  4442  frirr  4502  wereu2  4522  ordtri4  4561  oneqmini  4575  elsucg  4591  elsuc2g  4592  dfwe2  4704  ssonprc  4714  ordpwsuc  4737  dfom2  4789  brab2a  4869  opeliunxp  4871  posn  4888  sosn  4889  frsn  4890  brab2ga  4893  opbrop  4897  elrnmpt1  5061  elrnmptg  5062  eliniseg2  5186  poleloe  5210  cnvpo  5352  dffun8  5422  fncnv  5457  fununi  5459  fnssresb  5499  fnimaeq0  5508  funcocnv2  5642  dffn5  5713  funimass4  5718  fnsnfv  5727  dmfco  5738  fndmdif  5775  fvimacnvi  5785  fvimacnvALT  5790  unpreima  5797  respreima  5800  fmptco  5842  fressnfv  5861  fnsuppres  5893  elunirnALT  5941  dff13  5945  fliftel  5972  isoini  5999  f1oiso  6012  f1oweALT  6015  eloprabga  6101  resoprab2  6108  ralrnmpt2  6125  ovid  6131  ov  6134  ovg  6153  ofrfval2  6264  fmpt2x  6358  ovmptss  6369  1stconst  6376  2ndconst  6377  isprmpt2  6415  brtpos2  6423  dfsmo2  6547  tfrlem1  6574  rdglim2  6628  seqomlem2  6646  omeu  6766  oeeui  6783  brdifun  6870  eqerlem  6875  brecop  6935  erovlem  6938  eceqoveq  6947  mapsn  6993  mptelixpg  7037  map1  7123  xpsnen  7130  xpdom2  7141  omxpenlem  7147  xpf1o  7207  mapunen  7214  onfin  7235  fimaxg  7292  fodomfib  7324  fofinf1o  7325  fipreima  7349  supub  7399  ordtypecbv  7421  ordtypelem3  7424  ordtypelem9  7430  hartogslem1  7446  wofib  7449  wemapso2lem  7454  wemapso2  7456  noinfep  7549  noinfepOLD  7550  cantnf  7584  rankbnd2  7730  domtri2  7811  infxpenc2  7838  fseqdom  7842  acni2  7862  dfac9  7951  cfeq0  8071  cfsuc  8072  cflim3  8077  cfslb  8081  cofsmo  8084  enfin2i  8136  isfin3ds  8144  isf33lem  8181  fin1a2lem5  8219  axdc2lem  8263  zorn2g  8318  fodomb  8339  brdom7disj  8344  brdom6disj  8345  iundom2g  8350  cfpwsdom  8394  elgch  8432  fpwwe2cbv  8440  fpwwecbv  8454  pwfseqlem3  8470  pwfseqlem4a  8471  pwfseqlem4  8472  ltpiord  8699  nlt1pi  8718  nqereu  8741  addclprlem1  8828  1idpr  8841  reclem3pr  8861  ltsosr  8904  map2psrpr  8920  supsrlem  8921  axrrecex  8973  xrlenlt  9078  addsubeq4  9254  renegcli  9296  lesub0  9478  wloglei  9493  conjmul  9665  rereccl  9666  infm3  9901  supmul1  9907  supmullem1  9908  supmullem2  9909  supmul  9910  creui  9929  nndiv  9974  elznn0  10230  prime  10284  eqreznegel  10495  zsupss  10499  rebtwnz  10507  ltxr  10649  elixx3g  10863  ixxun  10866  ioo0  10875  ico0  10896  ioc0  10897  icc0  10898  difreicc  10962  iccf1o  10973  elfz2  10984  fzn  11005  fznn  11047  fzshftral  11066  fzosplitsni  11125  om2uzisoi  11223  sq11i  11401  hashsdom  11584  brfi1uzind  11644  wrdval  11659  s2f1o  11792  cjreb  11857  rexfiuz  12080  cau3lem  12087  rlim2  12219  ello12  12239  ello1mpt  12244  elo12  12250  o1lo1  12260  lo1resb  12287  o1resb  12289  o1compt  12310  caucvgb  12402  mertens  12592  ruclem12  12769  divides  12783  odd2np1  12837  oddm1even  12838  sadadd2lem2  12891  gcdcllem2  12941  bezoutlem2  12968  bezoutlem3  12969  bezoutlem4  12970  isprm2  13016  isprm3  13017  prmreclem2  13214  prmreclem5  13217  prmreclem6  13218  4sqlem2  13246  4sqlem12  13253  vdwmc  13275  vdwpc  13277  vdwlem6  13283  vdwlem10  13287  vdwnn  13295  ramval  13305  0ram  13317  prdsleval  13628  pwsle  13643  imasleval  13695  xpsfrnel2  13719  xpsle  13735  isacs2  13807  mreacs  13812  acsfn  13813  iscatd2  13835  catpropd  13864  isssc  13949  evlfcl  14248  uncfcurf  14265  pltval  14346  lubid  14368  tosso  14394  oduleg  14488  oduclatb  14500  isipodrs  14516  odudlatb  14551  spwpr2  14589  spwex  14590  gsumvalx  14703  grplmulf1o  14794  grplactcnv  14816  elnmz  14908  eqgid  14921  isghm  14935  ghmeqker  14961  resscntz  15059  odmulgeq  15122  sylow3lem3  15192  sylow3lem6  15195  efgval2  15285  efgsdm  15291  efgrelexlema  15310  efgcpbllemb  15316  iscyggen2  15420  cyggenod  15423  eldprd  15491  dprdf11  15510  dprddisj2  15526  pgpfac1lem2  15562  pgpfac1  15567  drngid2  15780  issubrg  15797  islmod  15883  aspval2  16334  psrbag  16360  zndvds  16755  znleval  16760  iunocv  16833  pjfval2  16861  pjdm2  16863  istopg  16893  istpsOLD  16910  basgen2  16979  isclo  17076  mretopd  17081  isnei  17092  isperf3  17141  restdis  17166  neitr  17168  restcls  17169  restlp  17171  restperf  17172  iscn  17223  iscnp  17225  lmbr2  17247  lmbrf  17248  ordtt1  17367  cmpsub  17387  hauscmplem  17393  cmpfi  17395  dfcon2  17405  1stcelcls  17447  1stccn  17449  nllyi  17461  subislly  17467  elkgen  17491  ptpjpre1  17526  ptuni2  17531  ptclsg  17570  ptcnplem  17576  txcn  17581  hausdiag  17600  txhaus  17602  txkgen  17607  xkoptsub  17609  cnmpt21  17626  elqtop  17652  tgqtop  17667  r0cld  17693  elfg  17826  fbasrn  17839  trfil2  17842  trfil3  17843  fin1aufil  17887  elfm2  17903  elfm3  17905  flimopn  17930  fbflim  17931  flfnei  17946  flftg  17951  cnpflf2  17955  txflf  17961  fclsbas  17976  alexsubALTlem4  18004  cnextfvval  18019  snclseqg  18068  tgphaus  18069  tsmsfbas  18080  tsmssubm  18095  utopsnneip  18201  prdsxmetlem  18308  imasdsf1olem  18313  xpsdsval  18321  blres  18353  isxms2  18370  metcnp  18463  txmetcnp  18469  txmetcn  18470  metustel  18472  metuel2  18487  dscopn  18494  isngp4  18531  cnblcld  18682  metnrmlem1a  18761  icoopnst  18837  iocopnst  18838  elpi1  18943  lmmbr2  19085  cfil3i  19095  caucfil  19109  iscmet3  19119  lmclim  19128  metcld2  19132  bcthlem4  19151  minveclem3b  19198  minveclem6  19204  minveclem7  19205  ivthle  19222  ivthle2  19223  evthicc2  19226  ovolfioo  19233  ovolficc  19234  ovolgelb  19245  dyadmax  19359  subopnmbl  19365  ismbf3d  19415  mbfimaopnlem  19416  mbfimaopn2  19418  mbfaddlem  19421  mbfsup  19425  mbfinf  19426  i1f1lem  19450  i1fmulclem  19463  itg1climres  19475  mbfi1fseqlem4  19479  itg2monolem1  19511  itg2gt0  19521  isibl  19526  iblcnlem1  19548  ellimc2  19633  dvcnvrelem1  19770  itgsubst  19802  mdegleb  19856  fta1glem2  19958  quotval  20078  vieta1lem1  20096  vieta1lem2  20097  ulm2  20170  ulmcaulem  20179  ulmcau  20180  radcnvlt1  20203  sineq0  20298  cos11  20304  recosf1o  20306  efopn  20418  cxpeq  20510  mcubic  20556  birthdaylem3  20661  rlimcnp  20673  xrlimcnp  20676  wilth  20723  isppw  20766  isppw2  20767  mumullem2  20832  sqff1o  20834  dvdsmulf1o  20848  fsumvma  20866  fsumvma2  20867  vmasum  20869  chpchtsum  20872  lgsne0  20986  lgseisenlem2  21003  lgsquadlem1  21007  lgsquadlem2  21008  dchrmusumlema  21056  rpvmasum2  21075  dchrisum0lema  21077  pntibndlem3  21155  pntlemi  21167  pntleml  21174  pnt3  21175  nbgraf1olem1  21319  nbgraf1olem5  21323  nbcusgra  21340  uvtx01vtx  21369  cusgrauvtxb  21373  iswlk  21393  istrl  21403  ispth  21424  isspth  21425  wlkdvspthlem  21457  usgrcyclnl2  21478  eupath2  21552  grpodiveq  21694  opidon  21760  issmgrp  21772  ismndo  21781  isrngo  21816  isdivrngo  21869  isvclem  21906  isnvlem  21939  isphg  22168  isph  22173  phoeqi  22209  ubthlem3  22224  minvecolem5  22233  minvecolem6  22234  minvecolem7  22235  hhph  22530  issh3  22572  nmopub  23261  nmfnleub  23278  adjeq  23288  adjvalval  23290  elunop2  23366  lnophm  23372  nmcexi  23379  cnlnadjlem5  23424  cnlnadjeui  23430  adjbd1o  23438  jpi  23623  mddmd2  23662  chrelati  23717  chrelat2i  23718  cvexchlem  23721  dmdbr5ati  23775  cdjreui  23785  cdj3i  23794  preqsnd  23846  abfmpunirn  23908  feqmptdf  23919  fmptcof2  23920  funcnvmptOLD  23925  funcnvmpt  23926  funcnv5mpt  23927  iocinioc2  23980  eliccioo  24018  xrmulc1cn  24122  isrrvv  24482  eldmgm  24587  dmgmaddn0  24588  lgamgulmlem6  24599  subfacp1lem3  24649  subfacp1lem6  24652  subfacp1  24653  txpcon  24700  sconpi1  24707  rescon  24714  cvmscbv  24726  cvmsval  24734  cvmlift2lem13  24783  cvmlift3lem2  24788  cvmlift3  24796  divelunit  24966  br8  25139  br6  25140  br4  25141  distel  25186  elpred  25203  poseq  25279  sltsolem1  25348  elfuns  25480  imageval  25495  funpartfv  25510  dfrdg4  25515  altopthg  25528  altopthbg  25529  brbtwn  25554  brcgr  25555  brbtwn2  25560  colinearalg  25565  axeuclidlem  25617  axcontlem2  25620  axcontlem4  25622  axcontlem7  25625  brcolinear2  25708  lineext  25726  brsegle  25758  seglelin  25766  broutsideof2  25772  bpolyval  25811  onsuct0  25907  supaddc  25949  supadd  25950  itg2addnclem2  25960  isfne4  26042  isfne2  26044  isfne3  26045  fneval  26060  topfneec  26064  neibastop2lem  26082  neibastop2  26083  neifg  26093  filnetlem4  26103  fdc  26142  heibor1  26212  rrncmslem  26234  rrnheibor  26239  isfldidl2  26372  isdmn3  26377  prtlem13  26410  prter3  26424  fnnfpeq0  26432  ralxpxfr2d  26434  ellz1  26518  lzunuz  26519  fz1eqin  26520  diophrex  26527  rexrabdioph  26547  rexfrabdioph  26548  2rexfrabdioph  26549  3rexfrabdioph  26550  4rexfrabdioph  26551  6rexfrabdioph  26552  7rexfrabdioph  26553  fzneg  26740  expdioph  26787  wepwsolem  26809  fnwe2lem2  26819  islmodfg  26838  kercvrlsm  26852  dsmmelbas  26876  ellspd  26925  islindf  26953  islindf4  26979  f1omvdconj  27060  sdrgacs  27180  pm10.52  27231  iotasbc  27290  pm14.122a  27293  pm14.122b  27294  pm14.123a  27296  rusbcALT  27310  fvsb  27325  stoweidlem34  27453  2reu4a  27637  sbcfun  27657  funressnfv  27663  dfafn5a  27695  frgra3vlem2  27756  frgrancvvdeqlem2  27785  frgrancvvdeqlem3  27786  frgrancvvdeqlemC  27793  gte-lte  27815  gt-lt  27816  bnj976  28488  bnj944  28649  bnj1173  28711  bnj1321  28736  bnj1373  28739  bnj1417  28750  ax12olem6NEW7  28799  sbcomwAUX7  28925  sbcomOLD7  29073  lrelat  29131  islshpat  29134  lshpsmreu  29226  lkrpssN  29280  cmtvalN  29328  omllaw2N  29361  cvrval  29386  cvrval2  29391  cvlsupr3  29461  3dim0  29573  islln2  29627  islpln5  29651  islpln2  29652  islpln2ah  29665  islvol5  29695  islvol2  29696  4atlem11  29725  pmapglbx  29885  cdleme18d  30411  cdlemefrs29bpre0  30512  cdlemb3  30722  cdlemg33b  30823  dvhb1dimN  31102  dia11N  31165  cdlemm10N  31235  dib11N  31277  dib1dim  31282  dibglbN  31283  diblsmopel  31288  dihopelvalcpre  31365  dih11  31382  dihmeetlem4preN  31423  dihmeetlem13N  31436  lcfrvalsnN  31658  lcfrlem9  31667  lcf1o  31668  mapdval4N  31749  baerlem3lem2  31827  baerlem5alem2  31828  baerlem5blem2  31829  hdmap1fval  31914  hdmapfval  31947  hdmapglem7a  32047  hlhillcs  32078
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