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  1734  ax12olem6OLD  1982  sbcom  2146  abbi  2522  necon3abid  2608  necon3bid  2610  necon1abid  2628  r19.21t  2759  ceqsralt  2947  ceqsrexv  3037  ceqsrex2v  3039  elab2g  3052  elrabf  3059  eueq2  3076  eqreu  3094  reu8  3098  ru  3128  sbcralt  3201  csbnestgf  3267  disjpss  3646  ralprg  3825  rexprg  3826  difsn  3901  opthpr  3944  ralunsn  3971  dfiin2g  4092  iunxsng  4137  elpwuni  4146  disjxun  4178  pwnss  4333  opelopabt  4435  opelopabga  4436  brabga  4437  dfid3  4467  frirr  4527  wereu2  4547  ordtri4  4586  oneqmini  4600  elsucg  4616  elsuc2g  4617  dfwe2  4729  ssonprc  4739  ordpwsuc  4762  dfom2  4814  brab2a  4894  opeliunxp  4896  posn  4913  sosn  4914  frsn  4915  brab2ga  4918  opbrop  4922  elrnmpt1  5086  elrnmptg  5087  eliniseg2  5211  poleloe  5235  cnvpo  5377  dffun8  5447  fncnv  5482  fununi  5484  fnssresb  5524  fnimaeq0  5533  funcocnv2  5667  dffn5  5739  funimass4  5744  fnsnfv  5753  dmfco  5764  fndmdif  5801  fvimacnvi  5811  fvimacnvALT  5816  unpreima  5823  respreima  5826  fmptco  5868  fressnfv  5887  fnsuppres  5919  elunirnALT  5967  dff13  5971  fliftel  5998  isoini  6025  f1oiso  6038  f1oweALT  6041  eloprabga  6127  resoprab2  6134  ralrnmpt2  6151  ovid  6157  ov  6160  ovg  6179  ofrfval2  6290  fmpt2x  6384  ovmptss  6395  1stconst  6402  2ndconst  6403  isprmpt2  6444  brtpos2  6452  dfsmo2  6576  tfrlem1  6603  rdglim2  6657  seqomlem2  6675  omeu  6795  oeeui  6812  brdifun  6899  eqerlem  6904  brecop  6964  erovlem  6967  eceqoveq  6976  mapsn  7022  mptelixpg  7066  map1  7152  xpsnen  7159  xpdom2  7170  omxpenlem  7176  xpf1o  7236  mapunen  7243  onfin  7264  fimaxg  7321  fodomfib  7353  fofinf1o  7354  fipreima  7378  supub  7428  ordtypecbv  7450  ordtypelem3  7453  ordtypelem9  7459  hartogslem1  7475  wofib  7478  wemapso2lem  7483  wemapso2  7485  noinfep  7578  noinfepOLD  7579  cantnf  7613  rankbnd2  7759  domtri2  7840  infxpenc2  7867  fseqdom  7871  acni2  7891  dfac9  7980  cfeq0  8100  cfsuc  8101  cflim3  8106  cfslb  8110  cofsmo  8113  enfin2i  8165  isfin3ds  8173  isf33lem  8210  fin1a2lem5  8248  axdc2lem  8292  zorn2g  8347  fodomb  8368  brdom7disj  8373  brdom6disj  8374  iundom2g  8379  cfpwsdom  8423  elgch  8461  fpwwe2cbv  8469  fpwwecbv  8483  pwfseqlem3  8499  pwfseqlem4a  8500  pwfseqlem4  8501  ltpiord  8728  nlt1pi  8747  nqereu  8770  addclprlem1  8857  1idpr  8870  reclem3pr  8890  ltsosr  8933  map2psrpr  8949  supsrlem  8950  axrrecex  9002  xrlenlt  9107  eqlei2  9148  addsubeq4  9284  renegcli  9326  lesub0  9508  wloglei  9523  conjmul  9695  rereccl  9696  infm3  9931  supmul1  9937  supmullem1  9938  supmullem2  9939  supmul  9940  creui  9959  nndiv  10004  elznn0  10260  prime  10314  eqreznegel  10525  zsupss  10529  rebtwnz  10537  ltxr  10679  elixx3g  10893  ixxun  10896  ioo0  10905  ico0  10926  ioc0  10927  icc0  10928  difreicc  10992  iccf1o  11003  elfz2  11014  fzn  11035  fznn  11078  fzshftral  11097  fzosplitsni  11159  om2uzisoi  11257  sq11i  11435  hashsdom  11618  brfi1uzind  11678  wrdval  11693  s2f1o  11826  cjreb  11891  rexfiuz  12114  cau3lem  12121  rlim2  12253  ello12  12273  ello1mpt  12278  elo12  12284  o1lo1  12294  lo1resb  12321  o1resb  12323  o1compt  12344  caucvgb  12436  mertens  12626  ruclem12  12803  divides  12817  odd2np1  12871  oddm1even  12872  sadadd2lem2  12925  gcdcllem2  12975  bezoutlem2  13002  bezoutlem3  13003  bezoutlem4  13004  isprm2  13050  isprm3  13051  prmreclem2  13248  prmreclem5  13251  prmreclem6  13252  4sqlem2  13280  4sqlem12  13287  vdwmc  13309  vdwpc  13311  vdwlem6  13317  vdwlem10  13321  vdwnn  13329  ramval  13339  0ram  13351  prdsleval  13662  pwsle  13677  imasleval  13729  xpsfrnel2  13753  xpsle  13769  isacs2  13841  mreacs  13846  acsfn  13847  iscatd2  13869  catpropd  13898  isssc  13983  evlfcl  14282  uncfcurf  14299  pltval  14380  lubid  14402  tosso  14428  oduleg  14522  oduclatb  14534  isipodrs  14550  odudlatb  14585  spwpr2  14623  spwex  14624  gsumvalx  14737  grplmulf1o  14828  grplactcnv  14850  elnmz  14942  eqgid  14955  isghm  14969  ghmeqker  14995  resscntz  15093  odmulgeq  15156  sylow3lem3  15226  sylow3lem6  15229  efgval2  15319  efgsdm  15325  efgrelexlema  15344  efgcpbllemb  15350  iscyggen2  15454  cyggenod  15457  eldprd  15525  dprdf11  15544  dprddisj2  15560  pgpfac1lem2  15596  pgpfac1  15601  drngid2  15814  issubrg  15831  islmod  15917  aspval2  16368  psrbag  16394  zndvds  16793  znleval  16798  iunocv  16871  pjfval2  16899  pjdm2  16901  istopg  16931  istpsOLD  16948  basgen2  17017  isclo  17114  mretopd  17119  isnei  17130  isperf3  17179  restdis  17204  neitr  17206  restcls  17207  restlp  17209  restperf  17210  iscn  17261  iscnp  17263  lmbr2  17285  lmbrf  17286  ordtt1  17405  cmpsub  17425  hauscmplem  17431  cmpfi  17433  dfcon2  17443  1stcelcls  17485  1stccn  17487  nllyi  17499  subislly  17505  elkgen  17529  ptpjpre1  17564  ptuni2  17569  ptclsg  17608  ptcnplem  17614  txcn  17619  hausdiag  17638  txhaus  17640  txkgen  17645  xkoptsub  17647  cnmpt21  17664  elqtop  17690  tgqtop  17705  r0cld  17731  elfg  17864  fbasrn  17877  trfil2  17880  trfil3  17881  fin1aufil  17925  elfm2  17941  elfm3  17943  flimopn  17968  fbflim  17969  flfnei  17984  flftg  17989  cnpflf2  17993  txflf  17999  fclsbas  18014  alexsubALTlem4  18042  cnextfvval  18057  snclseqg  18106  tgphaus  18107  tsmsfbas  18118  tsmssubm  18133  utopsnneip  18239  prdsxmetlem  18359  imasdsf1olem  18364  xpsdsval  18372  blres  18422  isxms2  18439  metcnp  18532  txmetcnp  18538  txmetcn  18539  metustelOLD  18542  metustel  18543  metuel2  18570  dscopn  18582  isngp4  18619  cnblcld  18770  metnrmlem1a  18849  icoopnst  18925  iocopnst  18926  elpi1  19031  lmmbr2  19173  cfil3i  19183  caucfil  19197  iscmet3  19207  lmclim  19216  metcld2  19220  bcthlem4  19241  minveclem3b  19290  minveclem6  19296  minveclem7  19297  ivthle  19314  ivthle2  19315  evthicc2  19318  ovolfioo  19325  ovolficc  19326  ovolgelb  19337  dyadmax  19451  subopnmbl  19457  ismbf3d  19507  mbfimaopnlem  19508  mbfimaopn2  19510  mbfaddlem  19513  mbfsup  19517  mbfinf  19518  i1f1lem  19542  i1fmulclem  19555  itg1climres  19567  mbfi1fseqlem4  19571  itg2monolem1  19603  itg2gt0  19613  isibl  19618  iblcnlem1  19640  ellimc2  19725  dvcnvrelem1  19862  itgsubst  19894  mdegleb  19948  fta1glem2  20050  quotval  20170  vieta1lem1  20188  vieta1lem2  20189  ulm2  20262  ulmcaulem  20271  ulmcau  20272  radcnvlt1  20295  sineq0  20390  cos11  20396  recosf1o  20398  efopn  20510  cxpeq  20602  mcubic  20648  birthdaylem3  20753  rlimcnp  20765  xrlimcnp  20768  wilth  20815  isppw  20858  isppw2  20859  mumullem2  20924  sqff1o  20926  dvdsmulf1o  20940  fsumvma  20958  fsumvma2  20959  vmasum  20961  chpchtsum  20964  lgsne0  21078  lgseisenlem2  21095  lgsquadlem1  21099  lgsquadlem2  21100  dchrmusumlema  21148  rpvmasum2  21167  dchrisum0lema  21169  pntibndlem3  21247  pntlemi  21259  pntleml  21266  pnt3  21267  nbgraf1olem1  21412  nbgraf1olem5  21416  nbcusgra  21433  uvtx01vtx  21462  cusgrauvtxb  21466  iswlk  21488  istrl  21498  ispth  21529  isspth  21530  wlkdvspthlem  21568  usgrcyclnl2  21589  eupath2  21663  grpodiveq  21805  opidon  21871  issmgrp  21883  ismndo  21892  isrngo  21927  isdivrngo  21980  isvclem  22017  isnvlem  22050  isphg  22279  isph  22284  phoeqi  22320  ubthlem3  22335  minvecolem5  22344  minvecolem6  22345  minvecolem7  22346  hhph  22641  issh3  22683  nmopub  23372  nmfnleub  23389  adjeq  23399  adjvalval  23401  elunop2  23477  lnophm  23483  nmcexi  23490  cnlnadjlem5  23535  cnlnadjeui  23541  adjbd1o  23549  jpi  23734  mddmd2  23773  chrelati  23828  chrelat2i  23829  cvexchlem  23832  dmdbr5ati  23886  cdjreui  23896  cdj3i  23905  preqsnd  23961  abfmpunirn  24025  feqmptdf  24036  fmptcof2  24037  ofpreima  24042  funcnvmptOLD  24043  funcnvmpt  24044  funcnv5mpt  24045  iocinioc2  24103  eliccioo  24138  pstmxmet  24253  xrmulc1cn  24277  isrrvv  24662  eldmgm  24767  dmgmaddn0  24768  lgamgulmlem6  24779  subfacp1lem3  24829  subfacp1lem6  24832  subfacp1  24833  txpcon  24880  sconpi1  24887  rescon  24894  cvmscbv  24906  cvmsval  24914  cvmlift2lem13  24963  cvmlift3lem2  24968  cvmlift3  24976  divelunit  25146  br8  25335  br6  25336  br4  25337  distel  25382  elpred  25399  poseq  25475  sltsolem1  25544  elfuns  25676  imageval  25691  funpartfv  25706  dfrdg4  25711  altopthg  25724  altopthbg  25725  brbtwn  25750  brcgr  25751  brbtwn2  25756  colinearalg  25761  axeuclidlem  25813  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  brcolinear2  25904  lineext  25922  brsegle  25954  seglelin  25962  broutsideof2  25968  bpolyval  26007  onsuct0  26103  supaddc  26145  supadd  26146  mbfposadd  26161  cnambfre  26162  itg2addnclem2  26164  isfne4  26247  isfne2  26249  isfne3  26250  fneval  26265  topfneec  26269  neibastop2lem  26287  neibastop2  26288  neifg  26298  filnetlem4  26308  fdc  26347  heibor1  26417  rrncmslem  26439  rrnheibor  26444  isfldidl2  26577  isdmn3  26582  prtlem13  26615  prter3  26629  fnnfpeq0  26637  ralxpxfr2d  26639  ellz1  26723  lzunuz  26724  fz1eqin  26725  diophrex  26732  rexrabdioph  26752  rexfrabdioph  26753  2rexfrabdioph  26754  3rexfrabdioph  26755  4rexfrabdioph  26756  6rexfrabdioph  26757  7rexfrabdioph  26758  fzneg  26945  expdioph  26992  wepwsolem  27014  fnwe2lem2  27024  islmodfg  27043  kercvrlsm  27057  dsmmelbas  27081  ellspd  27130  islindf  27158  islindf4  27184  f1omvdconj  27265  sdrgacs  27385  pm10.52  27436  iotasbc  27495  pm14.122a  27498  pm14.122b  27499  pm14.123a  27501  rusbcALT  27515  fvsb  27530  stoweidlem34  27658  2reu4a  27842  sbcfun  27862  funressnfv  27867  dfafn5a  27899  el2xptp0  27957  otthg  27960  f12dfv  27969  f13dfv  27970  euhash1  28006  usgra2pthlem1  28048  usg2spthonot  28093  frgra3vlem2  28113  frgrancvvdeqlem2  28142  frgrancvvdeqlem3  28143  frgrancvvdeqlemC  28150  usg2spot2nb  28176  gte-lte  28189  gt-lt  28190  bnj976  28866  bnj944  29027  bnj1173  29089  bnj1321  29114  bnj1373  29117  bnj1417  29128  ax12olem6NEW7  29177  sbcomwAUX7  29303  sbcomOLD7  29451  lrelat  29509  islshpat  29512  lshpsmreu  29604  lkrpssN  29658  cmtvalN  29706  omllaw2N  29739  cvrval  29764  cvrval2  29769  cvlsupr3  29839  3dim0  29951  islln2  30005  islpln5  30029  islpln2  30030  islpln2ah  30043  islvol5  30073  islvol2  30074  4atlem11  30103  pmapglbx  30263  cdleme18d  30789  cdlemefrs29bpre0  30890  cdlemb3  31100  cdlemg33b  31201  dvhb1dimN  31480  dia11N  31543  cdlemm10N  31613  dib11N  31655  dib1dim  31660  dibglbN  31661  diblsmopel  31666  dihopelvalcpre  31743  dih11  31760  dihmeetlem4preN  31801  dihmeetlem13N  31814  lcfrvalsnN  32036  lcfrlem9  32045  lcf1o  32046  mapdval4N  32127  baerlem3lem2  32205  baerlem5alem2  32206  baerlem5blem2  32207  hdmap1fval  32292  hdmapfval  32325  hdmapglem7a  32425  hlhillcs  32456
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