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

Theorem syl5bb 251
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1
syl5bb.2
Assertion
Ref Expression
syl5bb

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3
21a1i 11 . 2
3 syl5bb.2 . 2
42, 3bitrd 247 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  syl5rbb  252  syl5bbr  253  3bitr4g  282  imim21b  360  cad0  1436  had1  1438  ax12wdemo  1762  sbcomOLD  2108  sbal2  2174  abbi  2532  necon3abid  2620  necon3bid  2622  necon1abid  2643  r19.21t  2780  ceqsralt  2975  ralxpxfr2d  3062  ceqsrexv  3071  ceqsrex2v  3073  elab2g  3086  elrabf  3093  eueq2  3111  eqreu  3129  reu8  3133  ru  3163  sbcralt  3244  sbcabel  3252  sbcel1g  3658  sbcel2  3660  csbnestgf  3669  sbccsb2  3680  disjpss  3706  sbcssg  3767  rexsng  3890  ralprg  3902  rexprg  3903  difsn  3983  opthpr  4025  ralunsn  4054  csbuni  4094  dfiin2g  4178  iunxsng  4224  elpwuni  4233  disjxun  4265  sbcbr12g  4321  pwnss  4429  opthneg  4543  opelopabt  4574  opelopabga  4575  brabga  4576  dfid3  4608  frirr  4668  wereu2  4688  ordtri4  4727  oneqmini  4741  elsucg  4757  elsuc2g  4758  brab2a  4859  opeliunxp  4861  posn  4878  sosn  4879  frsn  4880  brab2ga  4883  opbrop  4887  csbcnvgOLD  4995  elrnmpt1  5059  elrnmptg  5060  eliniseg2  5180  poleloe  5204  xpdifid  5238  cnvpo  5347  sbcfung  5413  dffun8  5417  fncnv  5452  fununi  5454  fnssresb  5493  fnimaeq0  5502  funcocnv2  5635  csbfv12  5695  dffn5  5707  funimass4  5712  fnsnfv  5721  dmfco  5735  fndmdif  5777  fvimacnvi  5787  fvimacnvALT  5792  unpreima  5799  respreima  5802  fmptco  5845  fressnfv  5865  fnnfpeq0  5878  fnsuppresOLD  5907  elunirnALT  5938  dff13  5939  fliftel  5970  isoini  5997  f1oiso  6010  eloprabga  6147  resoprab2  6157  elrnmpt2res  6174  ralrnmpt2  6175  ovid  6177  ov  6180  ovg  6199  ofrfval2  6307  dfwe2  6363  ssonprc  6373  ordpwsuc  6396  dfom2  6448  f1oweALT  6530  fmpt2x  6609  ovmptss  6623  1stconst  6630  2ndconst  6631  fnsuppres  6681  isprmpt2  6705  brtpos2  6713  dfsmo2  6767  rdglim2  6847  seqomlem2  6865  omeu  6985  oeeui  7002  brdifun  7089  eqerlem  7094  brecop  7154  erovlem  7157  eceqoveq  7166  mapsn  7213  ixpsnval  7225  mptelixpg  7259  map1  7347  xpsnen  7354  xpdom2  7365  omxpenlem  7371  xpf1o  7432  mapunen  7439  onfin  7460  fimaxg  7518  fodomfib  7550  fofinf1o  7551  fipreima  7576  supub  7656  ordtypecbv  7678  ordtypelem3  7681  ordtypelem9  7687  hartogslem1  7703  wofib  7706  wemapsolem  7711  wemapso2OLD  7713  wemapso2lem  7714  noinfep  7812  noinfepOLD  7813  cantnf  7848  cantnfOLD  7870  rankbnd2  8023  domtri2  8106  infxpenc2  8135  infxpenc2OLD  8139  fseqdom  8143  acni2  8163  dfac9  8252  cfeq0  8372  cfsuc  8373  cflim3  8378  cfslb  8382  cofsmo  8385  enfin2i  8437  isfin3ds  8445  isf33lem  8482  fin1a2lem5  8520  axdc2lem  8564  zorn2g  8619  fodomb  8640  brdom7disj  8645  brdom6disj  8646  iundom2g  8651  cfpwsdom  8695  elgch  8735  fpwwe2cbv  8743  fpwwecbv  8757  pwfseqlem3  8773  pwfseqlem4a  8774  pwfseqlem4  8775  ltpiord  9002  nlt1pi  9021  nqereu  9044  addclprlem1  9131  1idpr  9144  reclem3pr  9164  ltsosr  9207  map2psrpr  9223  supsrlem  9224  axrrecex  9276  xrlenlt  9388  eqlei2  9431  addsubeq4  9571  renegcli  9616  lesub0  9802  wloglei  9818  conjmul  9994  rereccl  9995  infm3  10235  supmul1  10241  supmullem1  10242  supmullem2  10243  supmul  10244  creui  10263  nndiv  10308  elznn0  10606  prime  10667  eqreznegel  10885  zsupss  10889  rebtwnz  10897  ltxr  11040  elixx3g  11258  ixxun  11261  ioo0  11270  ico0  11291  ioc0  11292  icc0  11293  difreicc  11361  divelunit  11371  iccf1o  11373  elfz2  11388  fzn  11410  fznn  11467  fzshftral  11488  fzosplitsni  11575  om2uzisoi  11718  sq11i  11897  hashsdom  12085  euhash1  12113  brfi1uzind  12160  wrdval  12179  csbwrdg  12198  wrd2ind  12313  s2f1o  12467  cjreb  12553  rexfiuz  12776  cau3lem  12783  rlim2  12915  ello12  12935  ello1mpt  12940  elo12  12946  o1lo1  12956  lo1resb  12983  o1resb  12985  o1compt  13006  caucvgb  13098  mertens  13286  ruclem12  13463  divides  13477  odd2np1  13532  oddm1even  13533  sadadd2lem2  13586  gcdcllem2  13636  bezoutlem2  13663  bezoutlem3  13664  bezoutlem4  13665  isprm2  13711  isprm3  13712  prmreclem2  13918  prmreclem5  13921  prmreclem6  13922  4sqlem2  13950  4sqlem12  13957  vdwmc  13979  vdwpc  13981  vdwlem6  13987  vdwlem10  13991  vdwnn  13999  ramval  14009  0ram  14021  prdsleval  14355  pwsle  14370  imasleval  14419  xpsfrnel2  14443  xpsle  14459  isacs2  14531  mreacs  14536  acsfn  14537  iscatd2  14559  catpropd  14588  isssc  14673  evlfcl  14972  uncfcurf  14989  pltval  15070  lublecllem  15098  tosso  15146  oduleg  15242  oduclatb  15254  posglbmo  15257  isipodrs  15271  odudlatb  15306  gsumvalx  15441  grplmulf1o  15537  grplactcnv  15561  elnmz  15657  eqgid  15670  isghm  15684  ghmeqker  15710  resscntz  15786  symg1bas  15838  pgrpsubgsymgbi  15849  symgfixelq  15875  f1omvdconj  15889  odmulgeq  15995  sylow3lem3  16065  sylow3lem6  16068  efgval2  16158  efgsdm  16164  efgrelexlema  16183  efgcpbllemb  16189  iscyggen2  16294  cyggenod  16297  gsummptfzcl  16354  eldprd  16371  dprdf11  16390  dprddisj2  16406  pgpfac1lem2  16442  pgpfac1  16447  drngid2  16661  issubrg  16678  islmod  16765  aspval2  17225  psrbag  17251  zndvds  17690  znleval  17695  iunocv  17814  pjfval2  17842  pjdm2  17844  dsmmelbas  17872  ellspd  17930  islindf  17940  islindf4  17966  istopg  18212  istpsOLD  18229  basgen2  18298  isclo  18395  mretopd  18400  isnei  18411  isperf3  18461  restdis  18486  neitr  18488  restcls  18489  restlp  18491  restperf  18492  iscn  18543  iscnp  18545  lmbr2  18567  lmbrf  18568  ordtt1  18687  cmpsub  18707  hauscmplem  18713  cmpfi  18715  bwthOLD  18718  dfcon2  18727  1stcelcls  18769  1stccn  18771  nllyi  18783  subislly  18789  elkgen  18813  ptpjpre1  18848  ptuni2  18853  ptclsg  18892  ptcnplem  18898  txcn  18903  hausdiag  18922  txhaus  18924  txkgen  18929  xkoptsub  18931  cnmpt21  18948  elqtop  18974  tgqtop  18989  r0cld  19015  elfg  19148  fbasrn  19161  trfil2  19164  trfil3  19165  fin1aufil  19209  elfm2  19225  elfm3  19227  flimopn  19252  fbflim  19253  flfnei  19268  flftg  19273  cnpflf2  19277  txflf  19283  fclsbas  19298  alexsubALTlem4  19326  cnextfvval  19341  snclseqg  19390  tgphaus  19391  tsmsfbas  19402  tsmssubm  19417  utopsnneip  19523  prdsxmetlem  19643  imasdsf1olem  19648  xpsdsval  19656  blres  19706  isxms2  19723  metcnp  19816  txmetcnp  19822  txmetcn  19823  metustelOLD  19826  metustel  19827  metuel2  19854  dscopn  19866  isngp4  19903  cnblcld  20054  metnrmlem1a  20134  icoopnst  20211  iocopnst  20212  elpi1  20317  lmmbr2  20470  cfil3i  20480  caucfil  20494  iscmet3  20504  lmclim  20513  metcld2  20517  bcthlem4  20538  minveclem3b  20615  minveclem6  20621  minveclem7  20622  ivthle  20640  ivthle2  20641  evthicc2  20644  ovolfioo  20651  ovolficc  20652  ovolgelb  20663  dyadmax  20778  subopnmbl  20784  ismbf3d  20832  mbfimaopnlem  20833  mbfimaopn2  20835  mbfaddlem  20838  mbfsup  20842  mbfinf  20843  i1f1lem  20867  i1fmulclem  20880  itg1climres  20892  mbfi1fseqlem4  20896  itg2monolem1  20928  itg2gt0  20938  isibl  20943  iblcnlem1  20965  ellimc2  21052  dvcnvrelem1  21189  itgsubst  21221  mdegleb  21277  fta1glem2  21379  quotval  21499  vieta1lem1  21517  vieta1lem2  21518  ulm2  21591  ulmcaulem  21600  ulmcau  21601  radcnvlt1  21624  sineq0  21724  cos11  21730  recosf1o  21732  efopn  21844  cxpeq  21936  mcubic  21983  birthdaylem3  22088  rlimcnp  22100  xrlimcnp  22103  wilth  22150  isppw  22193  isppw2  22194  mumullem2  22259  sqff1o  22261  dvdsmulf1o  22275  fsumvma  22293  fsumvma2  22294  vmasum  22296  chpchtsum  22299  lgsne0  22413  lgseisenlem2  22430  lgsquadlem1  22434  lgsquadlem2  22435  dchrmusumlema  22483  rpvmasum2  22502  dchrisum0lema  22504  pntibndlem3  22582  pntlemi  22594  pntleml  22601  pnt3  22602  trgcgrg  22704  colcom  22727  colrot1  22728  lncom  22759  mirreu3  22780  brbtwn  22824  brcgr  22825  brbtwn2  22830  colinearalg  22835  axeuclidlem  22887  axcontlem2  22890  axcontlem4  22892  axcontlem7  22895  nbgraf1olem1  23029  nbgraf1olem5  23033  nbcusgra  23050  uvtx01vtx  23079  cusgrauvtxb  23083  iswlk  23105  istrl  23115  ispth  23146  isspth  23147  wlkdvspthlem  23185  usgrcyclnl2  23206  eupath2  23280  grpodiveq  23422  opidon  23488  issmgrp  23500  ismndo  23509  isrngo  23544  isdivrngo  23597  isvclem  23634  isnvlem  23667  isphg  23896  isph  23901  phoeqi  23937  ubthlem3  23952  minvecolem5  23961  minvecolem6  23962  minvecolem7  23963  hhph  24259  issh3  24301  nmopub  24991  nmfnleub  25008  adjeq  25018  adjvalval  25020  elunop2  25096  lnophm  25102  nmcexi  25109  cnlnadjlem5  25154  cnlnadjeui  25160  adjbd1o  25168  jpi  25353  mddmd2  25392  chrelati  25447  chrelat2i  25448  cvexchlem  25451  dmdbr5ati  25505  cdjreui  25515  cdj3i  25524  preqsnd  25581  disjunsn  25616  opabdm  25623  opabrn  25624  abfmpunirn  25647  feqmptdf  25658  fmptcof2  25659  ofpreima  25664  funcnvmptOLD  25666  funcnvmpt  25667  funcnv5mpt  25668  f1od2  25704  resf1o  25710  fpwrelmap  25713  negelrp  25717  iocinioc2  25747  eliccioo  25784  posrasymb  25796  isslmd  25922  pstmxmet  26033  prsdm  26053  prsrn  26054  ordtconlem1  26063  xrmulc1cn  26069  isrrvv  26529  eldmgm  26711  dmgmaddn0  26712  lgamgulmlem6  26723  subfacp1lem3  26773  subfacp1lem6  26776  subfacp1  26777  txpcon  26824  sconpi1  26831  rescon  26838  cvmscbv  26850  cvmsval  26858  cvmlift2lem13  26907  cvmlift3lem2  26912  cvmlift3  26920  br8  27268  br6  27269  br4  27270  distel  27319  elpred  27340  poseq  27416  wsuclem  27464  sltsolem1  27511  imageval  27663  funpartfv  27678  dfrdg4  27683  altopthg  27700  altopthbg  27701  brcolinear2  27791  lineext  27809  brsegle  27841  seglelin  27849  broutsideof2  27855  onsuct0  27990  wl-ax11-lem6  28075  supaddc  28088  supadd  28089  tan2h  28095  ptrest  28096  mbfposadd  28110  cnambfre  28111  itg2addnclem2  28115  isfne4  28212  isfne2  28214  isfne3  28215  fneval  28230  topfneec  28234  neibastop2lem  28252  neibastop2  28253  neifg  28263  filnetlem4  28273  fdc  28312  heibor1  28380  rrncmslem  28402  rrnheibor  28407  isfldidl2  28540  isdmn3  28545  prtlem13  28685  prter3  28699  ellz1  28778  lzunuz  28779  fz1eqin  28780  diophrex  28787  rexrabdioph  28805  rexfrabdioph  28806  2rexfrabdioph  28807  3rexfrabdioph  28808  4rexfrabdioph  28809  6rexfrabdioph  28810  7rexfrabdioph  28811  fzneg  28998  expdioph  29045  wepwsolem  29067  fnwe2lem2  29077  islmodfg  29095  kercvrlsm  29109  sdrgacs  29231  pm10.52  29290  iotasbc  29346  pm14.122a  29349  pm14.122b  29350  pm14.123a  29352  rusbcALT  29366  fvsb  29381  stoweidlem34  29503  2reu4a  29687  funressnfv  29708  dfafn5a  29740  el2xptp0  29801  otthg  29804  f12dfv  29820  f13dfv  29821  elfz2z  29872  usgra2pthlem1  29974  wwlkn0s  30013  wwlkextwrd  30034  usg2spthonot  30081  isclwlk0  30093  clwwlkn2  30112  eclclwwlkn1  30180  eleclclwwlkn  30181  hashecclwwlkn1  30182  usghashecclwwlk  30183  clwlkfclwwlk1hashn  30188  clwlkfoclwwlk  30192  isrgra  30217  isrusgra  30218  wwlkextproplem3  30236  frgra3vlem2  30267  frgrancvvdeqlem2  30298  frgrancvvdeqlem3  30299  frgrancvvdeqlemC  30306  usg2spot2nb  30332  opeliun2xp  30394  ellspdX  30521  snlindsntor  30589  gte-lte  30643  gt-lt  30644  trsbc  30824  bnj976  31349  bnj944  31509  bnj1173  31571  bnj1321  31596  bnj1373  31599  bnj1417  31610  bj-abbi  31792  bj-tagcg  31925  bj-projval  31936  lrelat  32096  islshpat  32099  lshpsmreu  32191  lkrpssN  32245  cmtvalN  32293  omllaw2N  32326  cvrval  32351  cvrval2  32356  cvlsupr3  32426  3dim0  32538  islln2  32592  islpln5  32616  islpln2  32617  islpln2ah  32630  islvol5  32660  islvol2  32661  4atlem11  32690  pmapglbx  32850  cdleme18d  33376  cdlemefrs29bpre0  33477  cdlemb3  33687  cdlemg33b  33788  cdlemkid3N  34014  cdlemkid4  34015  dvhb1dimN  34067  dia11N  34130  cdlemm10N  34200  dib11N  34242  dib1dim  34247  dibglbN  34248  diblsmopel  34253  dihopelvalcpre  34330  dih11  34347  dihmeetlem4preN  34388  dihmeetlem13N  34401  lcfrvalsnN  34623  lcfrlem9  34632  lcf1o  34633  mapdval4N  34714  baerlem3lem2  34792  baerlem5alem2  34793  baerlem5blem2  34794  hdmap1fval  34879  hdmapfval  34912  hdmapglem7a  35012  hlhillcs  35043
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