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

Theorem syl5bb 257
Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-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 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  syl5rbb  258  syl5bbr  259  3bitr4g  288  imim21b  367  ifptru  1388  ifpfal  1389  cad0  1467  had1  1470  ax12wdemo  1831  sbal2  2205  abbiOLD  2589  necon3abid  2703  necon1abidOLD  2706  necon3bid  2715  r19.21tOLD  2855  ceqsralt  3133  ralxpxfr2d  3224  ceqsrexv  3233  ceqsrex2v  3235  elab2g  3248  elrabf  3255  elrab3t  3256  eueq2  3273  eqreu  3291  reu8  3295  ru  3326  sbcralt  3408  sbcabel  3416  sbcel1g  3829  sbcel2  3831  csbnestgf  3840  sbccsb2  3851  disjpss  3877  sbcssg  3940  rexsng  4065  ralprg  4078  rexprg  4079  difsn  4164  opthpr  4208  ralunsn  4237  csbuni  4277  dfiin2g  4363  iunxsng  4409  elpwuni  4418  disjxun  4450  sbcbr12g  4506  pwnss  4617  opthneg  4731  otthg  4735  opelopabt  4764  opelopabga  4765  brabga  4766  csbmpt12  4786  dfid3  4801  frirr  4861  wereu2  4881  ordtri4  4920  oneqmini  4934  elsucg  4950  elsuc2g  4951  brab2a  5054  opeliunxp  5056  posn  5073  sosn  5074  frsn  5075  brab2ga  5080  opbrop  5084  csbcnvgALT  5192  elrnmpt1  5256  elrnmptg  5257  eliniseg2  5381  poleloe  5406  xpdifid  5440  cnvpo  5550  sbcfung  5616  dffun8  5620  fncnv  5657  fununi  5659  fnssresb  5698  fnimaeq0  5707  funcocnv2  5845  csbfv12  5906  dffn5  5918  funimass4  5924  fnsnfv  5933  dmfco  5947  fndmdif  5991  fvimacnvi  6001  fvimacnvALT  6006  unpreima  6013  respreima  6016  fmptco  6064  fressnfv  6085  fmptsnd  6093  fnnfpeq0  6102  fnsuppresOLD  6131  elunirn  6163  dff13  6166  f12dfv  6179  f13dfv  6180  fliftel  6207  isoini  6234  f1oiso  6247  eloprabga  6389  resoprab2  6399  elrnmpt2res  6416  ralrnmpt2  6417  ovid  6419  ov  6422  ovg  6441  ofrfval2  6557  dfwe2  6617  ssonprc  6627  ordpwsuc  6650  dfom2  6702  f1oweALT  6784  el2xptp0  6844  fmpt2x  6866  ovmptss  6881  1stconst  6888  2ndconst  6889  fnsuppres  6946  isprmpt2  6972  brtpos2  6980  mpt2curryd  7017  dfsmo2  7037  rdglim2  7117  seqomlem2  7135  omeu  7253  oeeui  7270  brdifun  7357  eqerlem  7362  brecop  7423  erovlem  7426  eceqoveq  7435  mapsn  7480  ixpsnval  7492  mptelixpg  7526  map1  7614  xpsnen  7621  xpdom2  7632  omxpenlem  7638  xpf1o  7699  mapunen  7706  onfin  7728  fimaxg  7787  fodomfib  7820  fofinf1o  7821  fipreima  7846  supub  7939  ordtypecbv  7963  ordtypelem3  7966  ordtypelem9  7972  hartogslem1  7988  wofib  7991  wemapsolem  7996  wemapso2OLD  7998  wemapso2lem  7999  noinfep  8097  noinfepOLD  8098  cantnf  8133  cantnfOLD  8155  rankbnd2  8308  domtri2  8391  infxpenc2  8420  infxpenc2OLD  8424  fseqdom  8428  acni2  8448  dfac9  8537  cfeq0  8657  cfsuc  8658  cflim3  8663  cfslb  8667  cofsmo  8670  enfin2i  8722  isfin3ds  8730  isf33lem  8767  fin1a2lem5  8805  axdc2lem  8849  zorn2g  8904  fodomb  8925  brdom7disj  8930  brdom6disj  8931  iundom2g  8936  cfpwsdom  8980  elgch  9021  fpwwe2cbv  9029  fpwwecbv  9043  pwfseqlem3  9059  pwfseqlem4a  9060  pwfseqlem4  9061  ltpiord  9286  nlt1pi  9305  nqereu  9328  addclprlem1  9415  1idpr  9428  reclem3pr  9448  ltsosr  9492  map2psrpr  9508  supsrlem  9509  axrrecex  9561  xrlenlt  9673  eqlei2  9716  addsubeq4  9858  renegcli  9903  lesub0  10094  wloglei  10110  conjmul  10286  rereccl  10287  infm3  10527  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  creui  10556  nndiv  10601  elznn0  10904  prime  10968  eqreznegel  11196  zsupss  11200  rebtwnz  11210  ltxr  11353  elixx3g  11571  ixxun  11574  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  difreicc  11681  divelunit  11691  iccf1o  11693  elfz2  11708  fzn  11731  fznn  11776  fzshftral  11795  fzosplitsni  11920  om2uzisoi  12065  rabssnn0fi  12095  mptnn0fsupp  12103  sq11i  12258  hashsdom  12449  brfi1uzind  12532  wrdval  12551  csbwrdg  12570  wrd2ind  12703  s2f1o  12864  cjreb  12956  rexfiuz  13180  cau3lem  13187  rlim2  13319  ello12  13339  ello1mpt  13344  elo12  13350  o1lo1  13360  lo1resb  13387  o1resb  13389  o1compt  13410  caucvgb  13502  mertens  13695  ruclem12  13974  divides  13988  odd2np1  14046  oddm1even  14047  sadadd2lem2  14100  gcdcllem2  14150  bezoutlem2  14177  bezoutlem3  14178  bezoutlem4  14179  isprm2  14225  isprm3  14226  prmreclem2  14435  prmreclem5  14438  prmreclem6  14439  4sqlem2  14467  4sqlem12  14474  vdwmc  14496  vdwpc  14498  vdwlem6  14504  vdwlem10  14508  vdwnn  14516  ramval  14526  0ram  14538  prdsleval  14874  pwsle  14889  imasleval  14938  xpsfrnel2  14962  xpsle  14978  isacs2  15050  mreacs  15055  acsfn  15056  iscatd2  15078  catpropd  15104  isssc  15189  evlfcl  15491  uncfcurf  15508  pltval  15590  lublecllem  15618  tosso  15666  oduleg  15762  oduclatb  15774  posglbmo  15777  isipodrs  15791  odudlatb  15826  gsumvalx  15897  sgrp2rid2  16044  grplmulf1o  16112  grplactcnv  16138  elnmz  16240  eqgid  16253  isghm  16267  ghmeqker  16293  resscntz  16369  symg1bas  16421  pgrpsubgsymgbi  16432  symgfixelq  16458  f1omvdconj  16471  odmulgeq  16579  sylow3lem3  16649  sylow3lem6  16652  efgval2  16742  efgsdm  16748  efgrelexlema  16767  efgcpbllemb  16773  iscyggen2  16884  cyggenod  16887  gsummptfzcl  16996  eldprd  17035  eldprdOLD  17037  dprdf11  17063  dprdf11OLD  17070  dprddisj2  17087  dprddisj2OLD  17088  pgpfac1lem2  17126  pgpfac1  17131  srg1zr  17180  drngid2  17412  issubrg  17429  islmod  17516  aspval2  17996  psrbag  18013  cply1coe0bi  18342  zndvds  18588  znleval  18593  iunocv  18712  pjfval2  18740  pjdm2  18742  dsmmelbas  18770  ellspd  18836  ellspdOLD  18837  islindf  18847  islindf4  18873  istopg  19404  istpsOLD  19421  basgen2  19491  isclo  19588  mretopd  19593  isnei  19604  isperf3  19654  restdis  19679  neitr  19681  restcls  19682  restlp  19684  restperf  19685  iscn  19736  iscnp  19738  lmbr2  19760  lmbrf  19761  ordtt1  19880  cmpsub  19900  hauscmplem  19906  cmpfi  19908  bwthOLD  19911  dfcon2  19920  1stcelcls  19962  1stccn  19964  nllyi  19976  subislly  19982  dissnlocfin  20030  elkgen  20037  ptpjpre1  20072  ptuni2  20077  ptclsg  20116  ptcnplem  20122  txcn  20127  hausdiag  20146  txhaus  20148  txkgen  20153  xkoptsub  20155  cnmpt21  20172  elqtop  20198  tgqtop  20213  r0cld  20239  elfg  20372  fbasrn  20385  trfil2  20388  trfil3  20389  fin1aufil  20433  elfm2  20449  elfm3  20451  flimopn  20476  fbflim  20477  flfnei  20492  flftg  20497  cnpflf2  20501  txflf  20507  fclsbas  20522  alexsubALTlem4  20550  cnextfvval  20565  snclseqg  20614  tgphaus  20615  tsmsfbas  20626  tsmssubm  20644  utopsnneip  20751  prdsxmetlem  20871  imasdsf1olem  20876  xpsdsval  20884  blres  20934  isxms2  20951  metcnp  21044  txmetcnp  21050  txmetcn  21051  metustelOLD  21054  metustel  21055  metuel2  21082  dscopn  21094  isngp4  21131  cnblcld  21282  metnrmlem1a  21362  icoopnst  21439  iocopnst  21440  elpi1  21545  lmmbr2  21698  cfil3i  21708  caucfil  21722  iscmet3  21732  lmclim  21741  metcld2  21745  bcthlem4  21766  minveclem3b  21843  minveclem6  21849  minveclem7  21850  ivthle  21868  ivthle2  21869  evthicc2  21872  ovolfioo  21879  ovolficc  21880  ovolgelb  21891  dyadmax  22007  subopnmbl  22013  ismbf3d  22061  mbfimaopnlem  22062  mbfimaopn2  22064  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  i1f1lem  22096  i1fmulclem  22109  itg1climres  22121  mbfi1fseqlem4  22125  itg2monolem1  22157  itg2gt0  22167  isibl  22172  iblcnlem1  22194  ellimc2  22281  dvcnvrelem1  22418  itgsubst  22450  mdegleb  22464  fta1glem2  22567  quotval  22688  vieta1lem1  22706  vieta1lem2  22707  ulm2  22780  ulmcaulem  22789  ulmcau  22790  radcnvlt1  22813  sineq0  22914  cos11  22920  recosf1o  22922  efopn  23039  cxpeq  23131  mcubic  23178  birthdaylem3  23283  rlimcnp  23295  xrlimcnp  23298  wilth  23345  isppw  23388  isppw2  23389  mumullem2  23454  sqff1o  23456  dvdsmulf1o  23470  fsumvma  23488  fsumvma2  23489  vmasum  23491  chpchtsum  23494  lgsne0  23608  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  dchrmusumlema  23678  rpvmasum2  23697  dchrisum0lema  23699  pntibndlem3  23777  pntlemi  23789  pntleml  23796  pnt3  23797  trgcgrg  23906  colcom  23945  colrot1  23946  ltgov  23983  hlcomb  23987  lncom  24002  mirreu3  24035  isperp  24089  perpcom  24090  brbtwn  24202  brcgr  24203  brbtwn2  24208  colinearalg  24213  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  nbgraf1olem1  24441  nbgraf1olem5  24445  nbcusgra  24463  uvtx01vtx  24492  cusgrauvtxb  24496  iswlk  24520  istrl  24539  ispth  24570  isspth  24571  wlkdvspthlem  24609  usgrcyclnl2  24641  wwlkn0s  24705  wwlkextwrd  24728  wwlkextproplem3  24743  isclwlk0  24754  clwwlkn2  24775  eclclwwlkn1  24832  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfclwwlk1hashn  24841  clwlkfoclwwlk  24845  usg2spthonot  24888  isrgra  24926  isrusgra  24927  isrusgusrg  24932  eupath2  24980  frgra3vlem2  25001  frgrancvvdeqlem2  25031  frgrancvvdeqlem3  25032  frgrancvvdeqlemC  25039  usg2spot2nb  25065  grpodiveq  25258  opidonOLD  25324  issmgrpOLD  25336  ismndo  25345  isrngo  25380  isdivrngo  25433  isvclem  25470  isnvlem  25503  isphg  25732  isph  25737  phoeqi  25773  ubthlem3  25788  minvecolem5  25797  minvecolem6  25798  minvecolem7  25799  hhph  26095  issh3  26137  nmopub  26827  nmfnleub  26844  adjeq  26854  adjvalval  26856  elunop2  26932  lnophm  26938  nmcexi  26945  cnlnadjlem5  26990  cnlnadjeui  26996  adjbd1o  27004  jpi  27189  mddmd2  27228  chrelati  27283  chrelat2i  27284  cvexchlem  27287  dmdbr5ati  27341  cdjreui  27351  cdj3i  27360  preqsnd  27418  disjunsn  27453  opeldifid  27456  fcoinvbr  27461  opabdm  27464  opabrn  27465  abfmpunirn  27490  feqmptdf  27501  fmptcof2  27502  funcnvmptOLD  27509  funcnvmpt  27510  funcnv5mpt  27511  f1od2  27547  resf1o  27553  fpwrelmap  27556  negelrp  27564  iocinioc2  27590  eliccioo  27627  posrasymb  27645  isslmd  27745  pstmxmet  27876  prsdm  27896  prsrn  27897  ordtconlem1  27906  xrmulc1cn  27912  eulerpartlemmf  28314  isrrvv  28382  eldmgm  28564  dmgmaddn0  28565  lgamgulmlem6  28576  subfacp1lem3  28626  subfacp1lem6  28629  subfacp1  28630  txpcon  28677  sconpi1  28684  rescon  28691  cvmscbv  28703  cvmsval  28711  cvmlift2lem13  28760  cvmlift3lem2  28765  cvmlift3  28773  mclsrcl  28921  br8  29185  br6  29186  br4  29187  distel  29236  elpred  29257  poseq  29333  wsuclem  29381  sltsolem1  29428  imageval  29580  funpartfv  29595  dfrdg4  29600  altopthg  29617  altopthbg  29618  brcolinear2  29708  lineext  29726  brsegle  29758  seglelin  29766  broutsideof2  29772  onsuct0  29906  wl-sbrimt  29998  wl-sblimt  29999  wl-sbnf1  30003  wl-mo2dnae  30019  wl-mo2t  30020  wl-mo3t  30021  wl-ax11-lem6  30030  supaddc  30041  supadd  30042  tan2h  30047  ptrest  30048  mbfposadd  30062  cnambfre  30063  itg2addnclem2  30067  isfne4  30158  isfne2  30160  isfne3  30161  fneval  30170  topfneec  30173  neibastop2lem  30178  neibastop2  30179  neifg  30189  filnetlem4  30199  fdc  30238  heibor1  30306  rrncmslem  30328  rrnheibor  30333  isfldidl2  30466  isdmn3  30471  prtlem13  30609  prter3  30623  ellz1  30700  lzunuz  30701  fz1eqin  30702  diophrex  30709  rexrabdioph  30727  rexfrabdioph  30728  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  fzneg  30920  expdioph  30965  wepwsolem  30987  fnwe2lem2  30997  islmodfg  31015  kercvrlsm  31029  sdrgacs  31150  pm10.52  31270  iotasbc  31326  pm14.122a  31329  pm14.122b  31330  pm14.123a  31332  rusbcALT  31346  fvsb  31361  limcperiod  31634  limsupre  31647  dvbdfbdioo  31727  stoweidlem34  31816  fourierdlem108  31997  fourierdlem110  31999  etransc  32066  2reu4a  32194  funressnfv  32213  dfafn5a  32245  elfz2z  32331  usgra2pthlem1  32353  isuhgr  32366  isushgr  32367  usgo0s0ALT  32436  usgo1s0ALT  32437  ismhm0  32493  tpres  32554  ciclcl  32586  cicrcl  32587  inclfusubc  32593  isrnghm  32698  rnghmval2  32701  uzlidlring  32735  lidldomnnring  32736  zrninitoringc  32879  opeliun2xp  32922  snlindsntor  33072  gte-lte  33118  gt-lt  33119  trsbc  33311  bnj976  33836  bnj944  33996  bnj1173  34058  bnj1321  34083  bnj1373  34086  bnj1417  34097  bj-abbi  34361  bj-tagcg  34543  bj-projval  34554  lrelat  34739  islshpat  34742  lshpsmreu  34834  lkrpssN  34888  cmtvalN  34936  omllaw2N  34969  cvrval  34994  cvrval2  34999  cvlsupr3  35069  3dim0  35181  islln2  35235  islpln5  35259  islpln2  35260  islpln2ah  35273  islvol5  35303  islvol2  35304  4atlem11  35333  pmapglbx  35493  cdleme18d  36020  cdlemefrs29bpre0  36122  cdlemb3  36332  cdlemg33b  36433  cdlemkid3N  36659  cdlemkid4  36660  dvhb1dimN  36712  dia11N  36775  cdlemm10N  36845  dib11N  36887  dib1dim  36892  dibglbN  36893  diblsmopel  36898  dihopelvalcpre  36975  dih11  36992  dihmeetlem4preN  37033  dihmeetlem13N  37046  lcfrvalsnN  37268  lcfrlem9  37277  lcf1o  37278  mapdval4N  37359  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  hdmap1fval  37524  hdmapfval  37557  hdmapglem7a  37657  hlhillcs  37688
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 185
  Copyright terms: Public domain W3C validator