MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bb Structured version   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  1409  had1  1411  ax11wdemo  1738  ax12olem6OLD  2016  sbcom  2164  sbcomOLD  2165  abbi  2546  necon3abid  2634  necon3bid  2636  necon1abid  2657  r19.21t  2791  ceqsralt  2979  ceqsrexv  3069  ceqsrex2v  3071  elab2g  3084  elrabf  3091  eueq2  3108  eqreu  3126  reu8  3130  ru  3160  sbcralt  3233  csbnestgf  3299  disjpss  3678  ralprg  3857  rexprg  3858  difsn  3933  opthpr  3976  ralunsn  4003  dfiin2g  4124  iunxsng  4169  elpwuni  4178  disjxun  4210  pwnss  4365  opelopabt  4467  opelopabga  4468  brabga  4469  dfid3  4499  frirr  4559  wereu2  4579  ordtri4  4618  oneqmini  4632  elsucg  4648  elsuc2g  4649  dfwe2  4762  ssonprc  4772  ordpwsuc  4795  dfom2  4847  brab2a  4927  opeliunxp  4929  posn  4946  sosn  4947  frsn  4948  brab2ga  4951  opbrop  4955  elrnmpt1  5119  elrnmptg  5120  eliniseg2  5244  poleloe  5268  cnvpo  5410  dffun8  5480  fncnv  5515  fununi  5517  fnssresb  5557  fnimaeq0  5566  funcocnv2  5700  dffn5  5772  funimass4  5777  fnsnfv  5786  dmfco  5797  fndmdif  5834  fvimacnvi  5844  fvimacnvALT  5849  unpreima  5856  respreima  5859  fmptco  5901  fressnfv  5920  fnsuppres  5952  elunirnALT  6000  dff13  6004  fliftel  6031  isoini  6058  f1oiso  6071  f1oweALT  6074  eloprabga  6160  resoprab2  6167  ralrnmpt2  6184  ovid  6190  ov  6193  ovg  6212  ofrfval2  6323  fmpt2x  6417  ovmptss  6428  1stconst  6435  2ndconst  6436  isprmpt2  6477  brtpos2  6485  dfsmo2  6609  tfrlem1  6636  rdglim2  6690  seqomlem2  6708  omeu  6828  oeeui  6845  brdifun  6932  eqerlem  6937  brecop  6997  erovlem  7000  eceqoveq  7009  mapsn  7055  mptelixpg  7099  map1  7185  xpsnen  7192  xpdom2  7203  omxpenlem  7209  xpf1o  7269  mapunen  7276  onfin  7297  fimaxg  7354  fodomfib  7386  fofinf1o  7387  fipreima  7412  supub  7464  ordtypecbv  7486  ordtypelem3  7489  ordtypelem9  7495  hartogslem1  7511  wofib  7514  wemapso2lem  7519  wemapso2  7521  noinfep  7614  noinfepOLD  7615  cantnf  7649  rankbnd2  7795  domtri2  7876  infxpenc2  7903  fseqdom  7907  acni2  7927  dfac9  8016  cfeq0  8136  cfsuc  8137  cflim3  8142  cfslb  8146  cofsmo  8149  enfin2i  8201  isfin3ds  8209  isf33lem  8246  fin1a2lem5  8284  axdc2lem  8328  zorn2g  8383  fodomb  8404  brdom7disj  8409  brdom6disj  8410  iundom2g  8415  cfpwsdom  8459  elgch  8497  fpwwe2cbv  8505  fpwwecbv  8519  pwfseqlem3  8535  pwfseqlem4a  8536  pwfseqlem4  8537  ltpiord  8764  nlt1pi  8783  nqereu  8806  addclprlem1  8893  1idpr  8906  reclem3pr  8926  ltsosr  8969  map2psrpr  8985  supsrlem  8986  axrrecex  9038  xrlenlt  9143  eqlei2  9184  addsubeq4  9320  renegcli  9362  lesub0  9544  wloglei  9559  conjmul  9731  rereccl  9732  infm3  9967  supmul1  9973  supmullem1  9974  supmullem2  9975  supmul  9976  creui  9995  nndiv  10040  elznn0  10296  prime  10350  eqreznegel  10561  zsupss  10565  rebtwnz  10573  ltxr  10715  elixx3g  10929  ixxun  10932  ioo0  10941  ico0  10962  ioc0  10963  icc0  10964  difreicc  11028  iccf1o  11039  elfz2  11050  fzn  11071  fznn  11115  fzshftral  11134  fzosplitsni  11196  om2uzisoi  11294  sq11i  11472  hashsdom  11655  brfi1uzind  11715  wrdval  11730  s2f1o  11863  cjreb  11928  rexfiuz  12151  cau3lem  12158  rlim2  12290  ello12  12310  ello1mpt  12315  elo12  12321  o1lo1  12331  lo1resb  12358  o1resb  12360  o1compt  12381  caucvgb  12473  mertens  12663  ruclem12  12840  divides  12854  odd2np1  12908  oddm1even  12909  sadadd2lem2  12962  gcdcllem2  13012  bezoutlem2  13039  bezoutlem3  13040  bezoutlem4  13041  isprm2  13087  isprm3  13088  prmreclem2  13285  prmreclem5  13288  prmreclem6  13289  4sqlem2  13317  4sqlem12  13324  vdwmc  13346  vdwpc  13348  vdwlem6  13354  vdwlem10  13358  vdwnn  13366  ramval  13376  0ram  13388  prdsleval  13699  pwsle  13714  imasleval  13766  xpsfrnel2  13790  xpsle  13806  isacs2  13878  mreacs  13883  acsfn  13884  iscatd2  13906  catpropd  13935  isssc  14020  evlfcl  14319  uncfcurf  14336  pltval  14417  lubid  14439  tosso  14465  oduleg  14559  oduclatb  14571  isipodrs  14587  odudlatb  14622  spwpr2  14660  spwex  14661  gsumvalx  14774  grplmulf1o  14865  grplactcnv  14887  elnmz  14979  eqgid  14992  isghm  15006  ghmeqker  15032  resscntz  15130  odmulgeq  15193  sylow3lem3  15263  sylow3lem6  15266  efgval2  15356  efgsdm  15362  efgrelexlema  15381  efgcpbllemb  15387  iscyggen2  15491  cyggenod  15494  eldprd  15562  dprdf11  15581  dprddisj2  15597  pgpfac1lem2  15633  pgpfac1  15638  drngid2  15851  issubrg  15868  islmod  15954  aspval2  16405  psrbag  16431  zndvds  16830  znleval  16835  iunocv  16908  pjfval2  16936  pjdm2  16938  istopg  16968  istpsOLD  16985  basgen2  17054  isclo  17151  mretopd  17156  isnei  17167  isperf3  17217  restdis  17242  neitr  17244  restcls  17245  restlp  17247  restperf  17248  iscn  17299  iscnp  17301  lmbr2  17323  lmbrf  17324  ordtt1  17443  cmpsub  17463  hauscmplem  17469  cmpfi  17471  bwth  17473  dfcon2  17482  1stcelcls  17524  1stccn  17526  nllyi  17538  subislly  17544  elkgen  17568  ptpjpre1  17603  ptuni2  17608  ptclsg  17647  ptcnplem  17653  txcn  17658  hausdiag  17677  txhaus  17679  txkgen  17684  xkoptsub  17686  cnmpt21  17703  elqtop  17729  tgqtop  17744  r0cld  17770  elfg  17903  fbasrn  17916  trfil2  17919  trfil3  17920  fin1aufil  17964  elfm2  17980  elfm3  17982  flimopn  18007  fbflim  18008  flfnei  18023  flftg  18028  cnpflf2  18032  txflf  18038  fclsbas  18053  alexsubALTlem4  18081  cnextfvval  18096  snclseqg  18145  tgphaus  18146  tsmsfbas  18157  tsmssubm  18172  utopsnneip  18278  prdsxmetlem  18398  imasdsf1olem  18403  xpsdsval  18411  blres  18461  isxms2  18478  metcnp  18571  txmetcnp  18577  txmetcn  18578  metustelOLD  18581  metustel  18582  metuel2  18609  dscopn  18621  isngp4  18658  cnblcld  18809  metnrmlem1a  18888  icoopnst  18964  iocopnst  18965  elpi1  19070  lmmbr2  19212  cfil3i  19222  caucfil  19236  iscmet3  19246  lmclim  19255  metcld2  19259  bcthlem4  19280  minveclem3b  19329  minveclem6  19335  minveclem7  19336  ivthle  19353  ivthle2  19354  evthicc2  19357  ovolfioo  19364  ovolficc  19365  ovolgelb  19376  dyadmax  19490  subopnmbl  19496  ismbf3d  19546  mbfimaopnlem  19547  mbfimaopn2  19549  mbfaddlem  19552  mbfsup  19556  mbfinf  19557  i1f1lem  19581  i1fmulclem  19594  itg1climres  19606  mbfi1fseqlem4  19610  itg2monolem1  19642  itg2gt0  19652  isibl  19657  iblcnlem1  19679  ellimc2  19764  dvcnvrelem1  19901  itgsubst  19933  mdegleb  19987  fta1glem2  20089  quotval  20209  vieta1lem1  20227  vieta1lem2  20228  ulm2  20301  ulmcaulem  20310  ulmcau  20311  radcnvlt1  20334  sineq0  20429  cos11  20435  recosf1o  20437  efopn  20549  cxpeq  20641  mcubic  20687  birthdaylem3  20792  rlimcnp  20804  xrlimcnp  20807  wilth  20854  isppw  20897  isppw2  20898  mumullem2  20963  sqff1o  20965  dvdsmulf1o  20979  fsumvma  20997  fsumvma2  20998  vmasum  21000  chpchtsum  21003  lgsne0  21117  lgseisenlem2  21134  lgsquadlem1  21138  lgsquadlem2  21139  dchrmusumlema  21187  rpvmasum2  21206  dchrisum0lema  21208  pntibndlem3  21286  pntlemi  21298  pntleml  21305  pnt3  21306  nbgraf1olem1  21451  nbgraf1olem5  21455  nbcusgra  21472  uvtx01vtx  21501  cusgrauvtxb  21505  iswlk  21527  istrl  21537  ispth  21568  isspth  21569  wlkdvspthlem  21607  usgrcyclnl2  21628  eupath2  21702  grpodiveq  21844  opidon  21910  issmgrp  21922  ismndo  21931  isrngo  21966  isdivrngo  22019  isvclem  22056  isnvlem  22089  isphg  22318  isph  22323  phoeqi  22359  ubthlem3  22374  minvecolem5  22383  minvecolem6  22384  minvecolem7  22385  hhph  22680  issh3  22722  nmopub  23411  nmfnleub  23428  adjeq  23438  adjvalval  23440  elunop2  23516  lnophm  23522  nmcexi  23529  cnlnadjlem5  23574  cnlnadjeui  23580  adjbd1o  23588  jpi  23773  mddmd2  23812  chrelati  23867  chrelat2i  23868  cvexchlem  23871  dmdbr5ati  23925  cdjreui  23935  cdj3i  23944  preqsnd  24000  abfmpunirn  24064  feqmptdf  24075  fmptcof2  24076  ofpreima  24081  funcnvmptOLD  24082  funcnvmpt  24083  funcnv5mpt  24084  iocinioc2  24142  eliccioo  24177  pstmxmet  24292  xrmulc1cn  24316  isrrvv  24701  eldmgm  24806  dmgmaddn0  24807  lgamgulmlem6  24818  subfacp1lem3  24868  subfacp1lem6  24871  subfacp1  24872  txpcon  24919  sconpi1  24926  rescon  24933  cvmscbv  24945  cvmsval  24953  cvmlift2lem13  25002  cvmlift3lem2  25007  cvmlift3  25015  divelunit  25185  br8  25379  br6  25380  br4  25381  distel  25431  elpred  25452  poseq  25528  wsuclem  25576  sltsolem1  25623  imageval  25775  funpartfv  25790  dfrdg4  25795  altopthg  25812  altopthbg  25813  brbtwn  25838  brcgr  25839  brbtwn2  25844  colinearalg  25849  axeuclidlem  25901  axcontlem2  25904  axcontlem4  25906  axcontlem7  25909  brcolinear2  25992  lineext  26010  brsegle  26042  seglelin  26050  broutsideof2  26056  onsuct0  26191  supaddc  26237  supadd  26238  mbfposadd  26254  cnambfre  26255  itg2addnclem2  26257  isfne4  26349  isfne2  26351  isfne3  26352  fneval  26367  topfneec  26371  neibastop2lem  26389  neibastop2  26390  neifg  26400  filnetlem4  26410  fdc  26449  heibor1  26519  rrncmslem  26541  rrnheibor  26546  isfldidl2  26679  isdmn3  26684  prtlem13  26717  prter3  26731  fnnfpeq0  26739  ralxpxfr2d  26741  ellz1  26825  lzunuz  26826  fz1eqin  26827  diophrex  26834  rexrabdioph  26854  rexfrabdioph  26855  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  fzneg  27047  expdioph  27094  wepwsolem  27116  fnwe2lem2  27126  islmodfg  27144  kercvrlsm  27158  dsmmelbas  27182  ellspd  27231  islindf  27259  islindf4  27285  f1omvdconj  27366  sdrgacs  27486  pm10.52  27537  iotasbc  27596  pm14.122a  27599  pm14.122b  27600  pm14.123a  27602  rusbcALT  27616  fvsb  27631  stoweidlem34  27759  2reu4a  27943  sbcfun  27963  funressnfv  27968  dfafn5a  28000  el2xptp0  28061  otthg  28064  f12dfv  28080  f13dfv  28081  elfz2z  28105  euhash1  28167  usgra2pthlem1  28310  usg2spthonot  28355  isrgra  28369  isrusgra  28370  frgra3vlem2  28391  frgrancvvdeqlem2  28420  frgrancvvdeqlem3  28421  frgrancvvdeqlemC  28428  usg2spot2nb  28454  gte-lte  28467  gt-lt  28468  bnj976  29148  bnj944  29309  bnj1173  29371  bnj1321  29396  bnj1373  29399  bnj1417  29410  ax12olem6NEW7  29459  sbcomwAUX7  29588  ax7w15lemAUX7  29667  ax7w15AUX7  29668  ax7w14AUX7  29670  sbcomOLD7  29755  lrelat  29812  islshpat  29815  lshpsmreu  29907  lkrpssN  29961  cmtvalN  30009  omllaw2N  30042  cvrval  30067  cvrval2  30072  cvlsupr3  30142  3dim0  30254  islln2  30308  islpln5  30332  islpln2  30333  islpln2ah  30346  islvol5  30376  islvol2  30377  4atlem11  30406  pmapglbx  30566  cdleme18d  31092  cdlemefrs29bpre0  31193  cdlemb3  31403  cdlemg33b  31504  dvhb1dimN  31783  dia11N  31846  cdlemm10N  31916  dib11N  31958  dib1dim  31963  dibglbN  31964  diblsmopel  31969  dihopelvalcpre  32046  dih11  32063  dihmeetlem4preN  32104  dihmeetlem13N  32117  lcfrvalsnN  32339  lcfrlem9  32348  lcf1o  32349  mapdval4N  32430  baerlem3lem2  32508  baerlem5alem2  32509  baerlem5blem2  32510  hdmap1fval  32595  hdmapfval  32628  hdmapglem7a  32728  hlhillcs  32759
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