MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bb Structured version   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 11 . 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 4    <-> wb 178
This theorem is referenced by:  syl5rbb  251  syl5bbr  252  3bitr4g  281  imim21b  358  cad0  1410  had1  1412  ax11wdemo  1741  ax12olem6OLD  2020  sbcom  2171  sbcomOLD  2172  abbi  2553  necon3abid  2641  necon3bid  2643  necon1abid  2664  r19.21t  2798  ceqsralt  2988  ceqsrexv  3078  ceqsrex2v  3080  elab2g  3093  elrabf  3100  eueq2  3117  eqreu  3135  reu8  3139  ru  3169  sbcralt  3249  sbcabel  3257  sbcel1g  3659  sbcel2  3661  csbnestgf  3670  sbccsb2  3683  disjpss  3706  ralprg  3886  rexprg  3887  difsn  3962  opthpr  4005  ralunsn  4032  dfiin2g  4154  iunxsng  4200  elpwuni  4209  disjxun  4241  pwnss  4400  opelopabt  4502  opelopabga  4503  brabga  4504  dfid3  4534  frirr  4594  wereu2  4614  ordtri4  4653  oneqmini  4667  elsucg  4683  elsuc2g  4684  dfwe2  4797  ssonprc  4807  ordpwsuc  4830  dfom2  4882  brab2a  4962  opeliunxp  4964  posn  4981  sosn  4982  frsn  4983  brab2ga  4986  opbrop  4990  elrnmpt1  5154  elrnmptg  5155  eliniseg2  5279  poleloe  5303  cnvpo  5445  dffun8  5515  fncnv  5550  fununi  5552  fnssresb  5592  fnimaeq0  5601  funcocnv2  5735  dffn5  5808  funimass4  5813  fnsnfv  5822  dmfco  5833  fndmdif  5870  fvimacnvi  5880  fvimacnvALT  5885  unpreima  5892  respreima  5895  fmptco  5937  fressnfv  5956  fnsuppres  5988  elunirnALT  6036  dff13  6040  fliftel  6067  isoini  6094  f1oiso  6107  f1oweALT  6110  eloprabga  6196  resoprab2  6203  ralrnmpt2  6220  ovid  6226  ov  6229  ovg  6248  ofrfval2  6359  fmpt2x  6453  ovmptss  6464  1stconst  6471  2ndconst  6472  isprmpt2  6513  brtpos2  6521  dfsmo2  6645  tfrlem1  6672  rdglim2  6726  seqomlem2  6744  omeu  6864  oeeui  6881  brdifun  6968  eqerlem  6973  brecop  7033  erovlem  7036  eceqoveq  7045  mapsn  7091  mptelixpg  7135  map1  7221  xpsnen  7228  xpdom2  7239  omxpenlem  7245  xpf1o  7305  mapunen  7312  onfin  7333  fimaxg  7390  fodomfib  7422  fofinf1o  7423  fipreima  7448  supub  7500  ordtypecbv  7522  ordtypelem3  7525  ordtypelem9  7531  hartogslem1  7547  wofib  7550  wemapso2lem  7555  wemapso2  7557  noinfep  7650  noinfepOLD  7651  cantnf  7685  rankbnd2  7831  domtri2  7914  infxpenc2  7941  fseqdom  7945  acni2  7965  dfac9  8054  cfeq0  8174  cfsuc  8175  cflim3  8180  cfslb  8184  cofsmo  8187  enfin2i  8239  isfin3ds  8247  isf33lem  8284  fin1a2lem5  8322  axdc2lem  8366  zorn2g  8421  fodomb  8442  brdom7disj  8447  brdom6disj  8448  iundom2g  8453  cfpwsdom  8497  elgch  8535  fpwwe2cbv  8543  fpwwecbv  8557  pwfseqlem3  8573  pwfseqlem4a  8574  pwfseqlem4  8575  ltpiord  8802  nlt1pi  8821  nqereu  8844  addclprlem1  8931  1idpr  8944  reclem3pr  8964  ltsosr  9007  map2psrpr  9023  supsrlem  9024  axrrecex  9076  xrlenlt  9181  eqlei2  9222  addsubeq4  9358  renegcli  9400  lesub0  9582  wloglei  9597  conjmul  9769  rereccl  9770  infm3  10005  supmul1  10011  supmullem1  10012  supmullem2  10013  supmul  10014  creui  10033  nndiv  10078  elznn0  10334  prime  10388  eqreznegel  10599  zsupss  10603  rebtwnz  10611  ltxr  10753  elixx3g  10967  ixxun  10970  ioo0  10979  ico0  11000  ioc0  11001  icc0  11002  difreicc  11066  iccf1o  11077  elfz2  11088  fzn  11109  fznn  11153  fzshftral  11172  fzosplitsni  11234  om2uzisoi  11332  sq11i  11510  hashsdom  11693  brfi1uzind  11753  wrdval  11768  s2f1o  11901  cjreb  11966  rexfiuz  12189  cau3lem  12196  rlim2  12328  ello12  12348  ello1mpt  12353  elo12  12359  o1lo1  12369  lo1resb  12396  o1resb  12398  o1compt  12419  caucvgb  12511  mertens  12701  ruclem12  12878  divides  12892  odd2np1  12946  oddm1even  12947  sadadd2lem2  13000  gcdcllem2  13050  bezoutlem2  13077  bezoutlem3  13078  bezoutlem4  13079  isprm2  13125  isprm3  13126  prmreclem2  13323  prmreclem5  13326  prmreclem6  13327  4sqlem2  13355  4sqlem12  13362  vdwmc  13384  vdwpc  13386  vdwlem6  13392  vdwlem10  13396  vdwnn  13404  ramval  13414  0ram  13426  prdsleval  13737  pwsle  13752  imasleval  13804  xpsfrnel2  13828  xpsle  13844  isacs2  13916  mreacs  13921  acsfn  13922  iscatd2  13944  catpropd  13973  isssc  14058  evlfcl  14357  uncfcurf  14374  pltval  14455  lubid  14477  tosso  14503  oduleg  14597  oduclatb  14609  isipodrs  14625  odudlatb  14660  spwpr2  14698  spwex  14699  gsumvalx  14812  grplmulf1o  14903  grplactcnv  14925  elnmz  15017  eqgid  15030  isghm  15044  ghmeqker  15070  resscntz  15168  odmulgeq  15231  sylow3lem3  15301  sylow3lem6  15304  efgval2  15394  efgsdm  15400  efgrelexlema  15419  efgcpbllemb  15425  iscyggen2  15529  cyggenod  15532  eldprd  15600  dprdf11  15619  dprddisj2  15635  pgpfac1lem2  15671  pgpfac1  15676  drngid2  15889  issubrg  15906  islmod  15992  aspval2  16443  psrbag  16469  zndvds  16868  znleval  16873  iunocv  16946  pjfval2  16974  pjdm2  16976  istopg  17006  istpsOLD  17023  basgen2  17092  isclo  17189  mretopd  17194  isnei  17205  isperf3  17255  restdis  17280  neitr  17282  restcls  17283  restlp  17285  restperf  17286  iscn  17337  iscnp  17339  lmbr2  17361  lmbrf  17362  ordtt1  17481  cmpsub  17501  hauscmplem  17507  cmpfi  17509  bwth  17511  dfcon2  17520  1stcelcls  17562  1stccn  17564  nllyi  17576  subislly  17582  elkgen  17606  ptpjpre1  17641  ptuni2  17646  ptclsg  17685  ptcnplem  17691  txcn  17696  hausdiag  17715  txhaus  17717  txkgen  17722  xkoptsub  17724  cnmpt21  17741  elqtop  17767  tgqtop  17782  r0cld  17808  elfg  17941  fbasrn  17954  trfil2  17957  trfil3  17958  fin1aufil  18002  elfm2  18018  elfm3  18020  flimopn  18045  fbflim  18046  flfnei  18061  flftg  18066  cnpflf2  18070  txflf  18076  fclsbas  18091  alexsubALTlem4  18119  cnextfvval  18134  snclseqg  18183  tgphaus  18184  tsmsfbas  18195  tsmssubm  18210  utopsnneip  18316  prdsxmetlem  18436  imasdsf1olem  18441  xpsdsval  18449  blres  18499  isxms2  18516  metcnp  18609  txmetcnp  18615  txmetcn  18616  metustelOLD  18619  metustel  18620  metuel2  18647  dscopn  18659  isngp4  18696  cnblcld  18847  metnrmlem1a  18926  icoopnst  19002  iocopnst  19003  elpi1  19108  lmmbr2  19250  cfil3i  19260  caucfil  19274  iscmet3  19284  lmclim  19293  metcld2  19297  bcthlem4  19318  minveclem3b  19367  minveclem6  19373  minveclem7  19374  ivthle  19391  ivthle2  19392  evthicc2  19395  ovolfioo  19402  ovolficc  19403  ovolgelb  19414  dyadmax  19528  subopnmbl  19534  ismbf3d  19582  mbfimaopnlem  19583  mbfimaopn2  19585  mbfaddlem  19588  mbfsup  19592  mbfinf  19593  i1f1lem  19617  i1fmulclem  19630  itg1climres  19642  mbfi1fseqlem4  19646  itg2monolem1  19678  itg2gt0  19688  isibl  19693  iblcnlem1  19715  ellimc2  19802  dvcnvrelem1  19939  itgsubst  19971  mdegleb  20025  fta1glem2  20127  quotval  20247  vieta1lem1  20265  vieta1lem2  20266  ulm2  20339  ulmcaulem  20348  ulmcau  20349  radcnvlt1  20372  sineq0  20467  cos11  20473  recosf1o  20475  efopn  20587  cxpeq  20679  mcubic  20725  birthdaylem3  20830  rlimcnp  20842  xrlimcnp  20845  wilth  20892  isppw  20935  isppw2  20936  mumullem2  21001  sqff1o  21003  dvdsmulf1o  21017  fsumvma  21035  fsumvma2  21036  vmasum  21038  chpchtsum  21041  lgsne0  21155  lgseisenlem2  21172  lgsquadlem1  21176  lgsquadlem2  21177  dchrmusumlema  21225  rpvmasum2  21244  dchrisum0lema  21246  pntibndlem3  21324  pntlemi  21336  pntleml  21343  pnt3  21344  nbgraf1olem1  21489  nbgraf1olem5  21493  nbcusgra  21510  uvtx01vtx  21539  cusgrauvtxb  21543  iswlk  21565  istrl  21575  ispth  21606  isspth  21607  wlkdvspthlem  21645  usgrcyclnl2  21666  eupath2  21740  grpodiveq  21882  opidon  21948  issmgrp  21960  ismndo  21969  isrngo  22004  isdivrngo  22057  isvclem  22094  isnvlem  22127  isphg  22356  isph  22361  phoeqi  22397  ubthlem3  22412  minvecolem5  22421  minvecolem6  22422  minvecolem7  22423  hhph  22718  issh3  22760  nmopub  23449  nmfnleub  23466  adjeq  23476  adjvalval  23478  elunop2  23554  lnophm  23560  nmcexi  23567  cnlnadjlem5  23612  cnlnadjeui  23618  adjbd1o  23626  jpi  23811  mddmd2  23850  chrelati  23905  chrelat2i  23906  cvexchlem  23909  dmdbr5ati  23963  cdjreui  23973  cdj3i  23982  preqsnd  24036  abfmpunirn  24099  feqmptdf  24110  fmptcof2  24111  ofpreima  24116  funcnvmptOLD  24117  funcnvmpt  24118  funcnv5mpt  24119  iocinioc2  24177  eliccioo  24212  pstmxmet  24327  xrmulc1cn  24351  isrrvv  24736  eldmgm  24841  dmgmaddn0  24842  lgamgulmlem6  24853  subfacp1lem3  24903  subfacp1lem6  24906  subfacp1  24907  txpcon  24954  sconpi1  24961  rescon  24968  cvmscbv  24980  cvmsval  24988  cvmlift2lem13  25037  cvmlift3lem2  25042  cvmlift3  25050  divelunit  25220  br8  25414  br6  25415  br4  25416  distel  25466  elpred  25487  poseq  25563  wsuclem  25611  sltsolem1  25658  imageval  25810  funpartfv  25825  dfrdg4  25830  altopthg  25847  altopthbg  25848  brbtwn  25873  brcgr  25874  brbtwn2  25879  colinearalg  25884  axeuclidlem  25936  axcontlem2  25939  axcontlem4  25941  axcontlem7  25944  brcolinear2  26027  lineext  26045  brsegle  26077  seglelin  26085  broutsideof2  26091  onsuct0  26226  supaddc  26273  supadd  26274  tan2h  26280  mbfposadd  26294  cnambfre  26295  itg2addnclem2  26299  isfne4  26391  isfne2  26393  isfne3  26394  fneval  26409  topfneec  26413  neibastop2lem  26431  neibastop2  26432  neifg  26442  filnetlem4  26452  fdc  26491  heibor1  26561  rrncmslem  26583  rrnheibor  26588  isfldidl2  26721  isdmn3  26726  prtlem13  26829  prter3  26843  fnnfpeq0  26851  ralxpxfr2d  26853  ellz1  26937  lzunuz  26938  fz1eqin  26939  diophrex  26946  rexrabdioph  26966  rexfrabdioph  26967  2rexfrabdioph  26968  3rexfrabdioph  26969  4rexfrabdioph  26970  6rexfrabdioph  26971  7rexfrabdioph  26972  fzneg  27159  expdioph  27206  wepwsolem  27228  fnwe2lem2  27238  islmodfg  27256  kercvrlsm  27270  dsmmelbas  27294  ellspd  27343  islindf  27371  islindf4  27397  f1omvdconj  27478  sdrgacs  27598  pm10.52  27649  iotasbc  27708  pm14.122a  27711  pm14.122b  27712  pm14.123a  27714  rusbcALT  27728  fvsb  27743  stoweidlem34  27871  2reu4a  28055  sbcfun  28075  funressnfv  28080  dfafn5a  28112  el2xptp0  28174  otthg  28177  f12dfv  28196  f13dfv  28197  elfz2z  28226  euhash1  28288  usgra2pthlem1  28446  usg2spthonot  28518  isrgra  28539  isrusgra  28540  frgra3vlem2  28563  frgrancvvdeqlem2  28592  frgrancvvdeqlem3  28593  frgrancvvdeqlemC  28600  usg2spot2nb  28626  gte-lte  28639  gt-lt  28640  bnj976  29322  bnj944  29483  bnj1173  29545  bnj1321  29570  bnj1373  29573  bnj1417  29584  ax12olem6NEW7  29633  sbcomwAUX7  29762  ax7w15lemAUX7  29841  ax7w15AUX7  29842  ax7w14AUX7  29844  sbcomOLD7  29929  lrelat  29986  islshpat  29989  lshpsmreu  30081  lkrpssN  30135  cmtvalN  30183  omllaw2N  30216  cvrval  30241  cvrval2  30246  cvlsupr3  30316  3dim0  30428  islln2  30482  islpln5  30506  islpln2  30507  islpln2ah  30520  islvol5  30550  islvol2  30551  4atlem11  30580  pmapglbx  30740  cdleme18d  31266  cdlemefrs29bpre0  31367  cdlemb3  31577  cdlemg33b  31678  dvhb1dimN  31957  dia11N  32020  cdlemm10N  32090  dib11N  32132  dib1dim  32137  dibglbN  32138  diblsmopel  32143  dihopelvalcpre  32220  dih11  32237  dihmeetlem4preN  32278  dihmeetlem13N  32291  lcfrvalsnN  32513  lcfrlem9  32522  lcf1o  32523  mapdval4N  32604  baerlem3lem2  32682  baerlem5alem2  32683  baerlem5blem2  32684  hdmap1fval  32769  hdmapfval  32802  hdmapglem7a  32902  hlhillcs  32933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator