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

Theorem syl5bb 275
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 271 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  syl5rbb  276  syl5bbr  277  3bitr4g  306  imim21b  385  ifpfal  1058  cad0  1675  ax12wdemo  2129  sbal2OLD  2541  eu6lem  2591  necon3abid  3005  necon3bid  3013  ralxpxfr2d  3530  ceqsrexv  3539  ceqsrex2v  3541  elab2g  3561  elrabf  3568  elrab3t  3571  eueq2  3592  eqreu  3610  reu8  3614  ru  3651  sbcralt  3728  sbcabel  3734  sbcel1g  4212  sbcel2  4214  csbnestgf  4221  sbccsb2  4231  disjpss  4253  sbcssg  4306  rexsngOLD  4440  rexsngf  4441  reusngf  4443  ralprgf  4461  rexprgf  4462  reuprg0  4469  difsn  4562  preq2b  4609  opthpr  4614  preqsnd  4622  preqsndOLD  4623  csbopg  4656  ralunsn  4659  csbuni  4703  dfiin2g  4788  iunxsng  4837  iunxsngf  4839  elpwuni  4852  disjxun  4886  sbcbr12g  4944  pwnss  5066  opthneg  5183  otthg  5187  opeqsng  5200  snopeqop  5204  opelopabt  5226  opelopabga  5227  brabga  5228  opelopabgf  5234  csbmpt12  5249  rbropapd  5254  dfid3  5264  frirr  5334  wereu2  5354  opeliunxp  5418  posn  5437  sosn  5438  frsn  5439  brab2a  5444  opbrop  5448  csbcnvgALT  5554  elrnmpt1  5622  elrnmptg  5623  opelres  5650  opelresgOLD2  5654  eliniseg2  5761  poleloe  5784  xpdifid  5818  cnvpo  5929  elpred  5948  ordtri4  6015  oneqmini  6029  elsucg  6045  elsuc2g  6046  sbcfung  6161  dffun8  6165  fncnv  6209  fununi  6211  fnssresb  6251  fnimaeq0  6261  csbfv12  6492  dffn5  6503  funimass4  6509  feqmptdf  6513  fnsnfv  6520  dmfco  6534  fndmdif  6586  fvimacnvi  6596  fvimacnvALT  6601  unpreima  6607  respreima  6610  fmptco  6663  fressnfv  6695  fmptsnd  6704  fnnfpeq0  6713  tpres  6740  elunirn  6783  dff13  6786  f12dfv  6803  f13dfv  6804  fliftel  6833  isoini  6862  f1oiso  6875  riotaeqimp  6908  fnbrovb  6972  eloprabga  7026  resoprab2  7036  elrnmpt2res  7053  ralrnmpt2  7054  ovid  7056  ov  7059  ovg  7078  ofrfval2  7194  dfwe2  7261  ssonprc  7272  ordpwsuc  7295  dfom2  7347  f1oweALT  7431  el2xptp0  7493  fmpt2x  7518  ovmptss  7541  1stconst  7548  2ndconst  7549  fnsuppres  7606  brtpos2  7642  mpt2curryd  7679  dfsmo2  7729  rdglim2  7813  seqomlem2  7831  omeu  7951  oeeui  7968  brdifun  8057  eqerlem  8062  brecop  8125  erovlem  8129  eceqoveq  8138  mapsnd  8185  ixpsnval  8199  mptelixpg  8233  xpsnen  8334  xpdom2  8345  omxpenlem  8351  xpf1o  8412  mapunen  8419  onfin  8441  fimaxg  8497  fodomfib  8530  fofinf1o  8531  fipreima  8562  supub  8655  infglb  8686  infglbb  8687  fiming  8694  fiinfg  8695  ordtypecbv  8713  ordtypelem3  8716  ordtypelem9  8722  hartogslem1  8738  wofib  8741  wemapsolem  8746  wemapso2lem  8748  noinfep  8856  cantnf  8889  rankbnd2  9031  domtri2  9150  infxpenc2  9180  fseqdom  9184  acni2  9204  dfac9  9295  cfeq0  9415  cfsuc  9416  cflim3  9421  cfslb  9425  cofsmo  9428  enfin2i  9480  isfin3ds  9488  isf33lem  9525  fin1a2lem5  9563  axdc2lem  9607  zorn2g  9662  fodomb  9685  brdom7disj  9690  brdom6disj  9691  iundom2g  9699  cfpwsdom  9743  elgch  9781  fpwwe2cbv  9789  fpwwecbv  9803  pwfseqlem3  9819  pwfseqlem4a  9820  pwfseqlem4  9821  ltpiord  10046  nlt1pi  10065  nqereu  10088  addclprlem1  10175  1idpr  10188  reclem3pr  10208  ltsosr  10253  map2psrpr  10269  supsrlem  10270  axrrecex  10322  xrlenlt  10444  eqlei2  10489  addsubeq4  10640  renegcli  10686  lesub0  10894  wloglei  10909  conjmul  11094  rereccl  11095  infm3  11340  supaddc  11348  supadd  11349  supmul1  11350  supmullem1  11351  supmullem2  11352  supmul  11353  creui  11373  nndiv  11425  elznn0  11747  prime  11814  eqreznegel  12085  zsupss  12088  rebtwnz  12098  negelrp  12176  ltxr  12264  elixx3g  12504  ixxun  12507  ioo0  12516  ico0  12537  ioc0  12538  icc0  12539  difreicc  12625  divelunit  12635  iccf1o  12637  elfz2  12654  fzn  12678  fznn  12730  fzshftral  12750  nelfzo  12798  fzosplitsni  12902  om2uzisoi  13076  rabssnn0fi  13108  mptnn0fsupp  13119  sq11i  13277  hashsdom  13489  fi1uzind  13597  wrdval  13606  csbwrdg  13637  wrd2ind  13848  wrd2indOLD  13849  s2f1o  14071  cjreb  14274  rexfiuz  14498  cau3lem  14505  rlim2  14639  ello12  14659  ello1mpt  14664  elo12  14670  o1lo1  14680  lo1resb  14707  o1resb  14709  o1compt  14730  caucvgb  14822  pwm1geoser  15008  mertens  15025  ruclem12  15378  divides  15393  dvdsabseq  15446  odd2np1  15473  oddm1even  15475  sumodd  15522  divalgmod  15540  modremain  15542  sadadd2lem2  15582  gcdcllem2  15632  bezoutlem2  15667  bezoutlem3  15668  bezoutlem4  15669  isprm2  15804  isprm3  15805  dvdsnprmd  15812  oddprmdvds  16015  prmreclem2  16029  prmreclem5  16032  prmreclem6  16033  4sqlem2  16061  4sqlem12  16068  vdwmc  16090  vdwpc  16092  vdwlem6  16098  vdwlem10  16102  vdwnn  16110  ramval  16120  0ram  16132  prdsleval  16527  pwsle  16542  imasleval  16591  xpsfrnel2  16615  xpsle  16631  isacs2  16703  mreacs  16708  acsfn  16709  iscatd2  16731  catpropd  16758  ciclcl  16851  cicrcl  16852  isssc  16869  evlfcl  17252  uncfcurf  17269  pltval  17350  lublecllem  17378  tosso  17426  oduleg  17522  oduclatb  17534  posglbmo  17537  isipodrs  17551  odudlatb  17586  gsumvalx  17660  sgrp2rid2  17804  grplmulf1o  17880  grplactcnv  17909  elnmz  18021  eqgid  18034  isghm  18048  ghmeqker  18075  resscntz  18151  symg1bas  18203  pgrpsubgsymgbi  18214  symgfixelq  18240  f1omvdconj  18253  odmulgeq  18362  sylow3lem3  18432  sylow3lem6  18435  efgval2  18525  efgsdm  18531  efgrelexlema  18552  efgcpbllemb  18558  iscyggen2  18673  cyggenod  18676  gsummptfzcl  18758  eldprd  18794  dprdf11  18813  dprddisj2  18829  pgpfac1lem2  18865  pgpfac1  18870  srg1zr  18920  drngid2  19159  issubrg  19176  islmod  19263  aspval2  19748  psrbag  19765  cply1coe0bi  20070  zndvds  20297  znleval  20302  iunocv  20428  pjfval2  20456  pjdm2  20458  dsmmelbas  20486  ellspd  20549  islindf  20559  islindf4  20585  istopg  21111  basgen2  21205  isclo  21303  mretopd  21308  isnei  21319  isperf3  21369  restdis  21394  neitr  21396  restcls  21397  restlp  21399  restperf  21400  iscn  21451  iscnp  21453  lmbr2  21475  lmbrf  21476  ordtt1  21595  cmpsub  21616  hauscmplem  21622  cmpfi  21624  dfconn2  21635  1stcelcls  21677  1stccn  21679  nllyi  21691  subislly  21697  dissnlocfin  21745  elkgen  21752  ptpjpre1  21787  ptuni2  21792  ptclsg  21831  ptcnplem  21837  txcn  21842  hausdiag  21861  txhaus  21863  txkgen  21868  xkoptsub  21870  cnmpt21  21887  elqtop  21913  tgqtop  21928  r0cld  21954  elfg  22087  fbasrn  22100  trfil2  22103  trfil3  22104  fin1aufil  22148  elfm2  22164  elfm3  22166  flimopn  22191  fbflim  22192  flfnei  22207  flftg  22212  cnpflf2  22216  txflf  22222  fclsbas  22237  alexsubALTlem4  22266  cnextfvval  22281  snclseqg  22331  tgphaus  22332  tsmsfbas  22343  tsmssubm  22358  utopsnneip  22464  prdsxmetlem  22585  imasdsf1olem  22590  xpsdsval  22598  blres  22648  isxms2  22665  metcnp  22758  txmetcnp  22764  txmetcn  22765  metustel  22767  metuel2  22782  dscopn  22790  isngp4  22828  cnblcld  22990  metnrmlem1a  23073  icoopnst  23150  iocopnst  23151  elpi1  23256  isclmp  23308  isncvsngp  23360  lmmbr2  23469  cfil3i  23479  caucfil  23493  iscmet3  23503  lmclim  23513  metcld2  23517  bcthlem4  23537  minveclem3b  23638  minveclem6  23644  minveclem7  23645  ivthle  23664  ivthle2  23665  evthicc2  23668  ovolfioo  23675  ovolficc  23676  ovolgelb  23688  dyadmax  23806  subopnmbl  23812  ismbf3d  23862  mbfimaopnlem  23863  mbfimaopn2  23865  mbfaddlem  23868  mbfsup  23872  mbfinf  23873  i1f1lem  23897  i1fmulclem  23910  itg1climres  23922  mbfi1fseqlem4  23926  itg2monolem1  23958  itg2gt0  23968  isibl  23973  iblcnlem1  23995  ellimc2  24082  dvcnvrelem1  24221  itgsubst  24253  mdegleb  24265  fta1glem2  24367  quotval  24488  vieta1lem1  24506  vieta1lem2  24507  ulm2  24580  ulmcaulem  24589  ulmcau  24590  radcnvlt1  24613  sineq0  24715  cos11  24721  recosf1o  24723  efopn  24845  cxpeq  24942  mcubic  25029  birthdaylem3  25136  rlimcnp  25148  xrlimcnp  25151  eldmgm  25204  dmgmaddn0  25205  lgamgulmlem6  25216  wilth  25253  isppw  25296  isppw2  25297  mumullem2  25362  sqff1o  25364  dvdsmulf1o  25376  fsumvma  25394  fsumvma2  25395  vmasum  25397  chpchtsum  25400  lgsne0  25516  gausslemma2dlem0i  25545  gausslemma2dlem1a  25546  lgseisenlem2  25557  lgsquadlem1  25561  lgsquadlem2  25562  2lgslem1a  25572  dchrmusumlema  25638  rpvmasum2  25657  dchrisum0lema  25659  pntibndlem3  25737  pntlemi  25749  pntleml  25756  pnt3  25757  trgcgrg  25870  tgcgr4  25886  colcom  25913  colrot1  25914  ltgov  25952  hlcomb  25958  lncom  25977  mirreu3  26009  isperp  26067  perpcom  26068  brbtwn  26252  brcgr  26253  brbtwn2  26258  colinearalg  26263  axeuclidlem  26315  axcontlem2  26318  axcontlem4  26320  axcontlem7  26323  elntg2  26338  edgiedgb  26406  isuhgr  26412  isushgr  26413  isupgr  26436  isumgr  26447  isuspgr  26505  isusgr  26506  uhgr0v0e  26589  isfusgrf1  26671  opfusgr  26674  usgr1v0e  26677  dfnbgr3  26689  nbuhgr2vtx1edgb  26703  edgnbusgreu  26718  edgnbusgreuOLD  26719  nbusgredgeu0  26720  isuvtx  26747  cusgruvtxb  26774  cplgr3v  26787  cusgrsizeinds  26804  vtxdg0v  26825  vtxd0nedgb  26840  vtxduhgr0nedg  26844  vtxdusgr0edgnelALT  26848  iswlk  26962  wlk1walk  26990  upgr2wlk  27019  upgristrl  27059  2pthnloop  27087  usgr2pthlem  27119  isclwlke  27133  isclwlkupgr  27134  iswwlksnx  27193  wwlksnextwrd  27265  wwlksnextwrdOLD  27270  wwlksnextproplem3  27291  wwlksnextproplem3OLD  27292  2pthon3v  27327  umgr2wlk  27333  elwwlks2on  27343  elwwlks2  27350  elwspths2spth  27351  clwwlknclwwlkdif  27363  clwlkclwwlk  27386  clwlkclwwlkOLD  27387  clwwlkn1  27435  clwwlkn2  27438  eclclwwlkn1  27477  eleclclwwlkn  27478  hashecclwwlkn1  27479  umgrhashecclwwlk  27480  clwwlknonel  27501  clwwlknon1  27503  clwwlknun  27518  1pthon2v  27560  uhgr3cyclex  27589  isconngr  27596  isconngr1  27597  eupthresOLD  27622  eupthres  27623  eupth2lems  27646  isfrgr  27670  frgr0v  27673  frgr3vlem2  27686  fusgr2wsp2nb  27746  extwwlkfab  27769  extwwlkfabOLD  27770  numclwwlk1lem2foa  27773  numclwwlk1lem2foaOLD  27774  numclwwlk1lem2fo  27778  numclwwlk1lem2foOLD  27783  isvclem  28008  isnvlem  28041  isphg  28248  isph  28253  phoeqi  28289  ubthlem3  28304  minvecolem5  28313  minvecolem6  28314  minvecolem7  28315  hhph  28611  issh3  28652  nmopub  29343  nmfnleub  29360  adjeq  29370  adjvalval  29372  elunop2  29448  lnophm  29454  nmcexi  29461  cnlnadjlem5  29506  cnlnadjeui  29512  adjbd1o  29520  jpi  29705  mddmd2  29744  chrelati  29799  chrelat2i  29800  cvexchlem  29803  dmdbr5ati  29857  cdjreui  29867  cdj3i  29876  disjunsn  29974  opeldifid  29979  fcoinvbr  29986  brabgaf  29987  opabdm  29990  opabrn  29991  iunsnima  29997  elimampt  30007  abfmpunirn  30021  fmptcof2  30026  funcnvmpt  30036  funcnv5mpt  30037  f1od2  30069  resf1o  30075  fpwrelmap  30078  iocinioc2  30109  eliccioo  30205  posrasymb  30223  isslmd  30321  smatrcl  30464  pstmxmet  30542  prsdm  30562  prsrn  30563  ordtconnlem1  30572  xrmulc1cn  30578  ispisys2  30818  elcarsg  30969  eulerpartlemmf  31039  isrrvv  31108  reprinrn  31302  tgoldbachgt  31347  bnj976  31451  bnj944  31611  bnj1173  31673  bnj1321  31698  bnj1373  31701  bnj1417  31712  subfacp1lem3  31767  subfacp1lem6  31770  subfacp1  31771  txpconn  31817  sconnpi1  31824  resconn  31831  cvmscbv  31843  cvmsval  31851  cvmlift2lem13  31900  cvmlift3lem2  31905  cvmlift3  31913  mclsrcl  32061  br8  32244  br6  32245  br4  32246  elintfv  32259  fv1stcnv  32272  fv2ndcnv  32273  distel  32301  frpomin  32331  poseq  32346  wsuclem  32363  sltsolem1  32419  nosupdm  32443  nosupbnd1lem4  32450  slenlt  32470  sleloe  32472  etasslt  32513  madeval2  32529  imageval  32630  funpartfv  32645  dfrdg4  32651  altopthg  32667  altopthbg  32668  brcolinear2  32758  lineext  32776  brsegle  32808  seglelin  32816  broutsideof2  32822  isfne4  32927  isfne2  32929  isfne3  32930  fneval  32939  topfneec  32942  neibastop2lem  32947  neibastop2  32948  neifg  32958  filnetlem4  32968  onsuct0  33027  bj-abbi  33356  bj-tagcg  33549  bj-projval  33560  bj-restuni  33627  bj-raldifsn  33631  csbwrecsg  33772  csboprabg  33775  csbmpt22g  33776  topdifinffinlem  33793  isbasisrelowllem1  33801  isbasisrelowllem2  33802  rdgeqoa  33816  csbfinxpg  33823  wl-sbrimt  33929  wl-sblimt  33930  wl-sbnf1  33934  wl-mo2df  33949  wl-eudf  33951  wl-mo2t  33954  wl-mo3t  33955  wl-ax11-lem6  33964  wl-dfclab  33970  wl-dfrabf  34002  uncov  34020  tan2h  34031  matunitlindf  34038  ptrest  34039  poimirlem2  34042  poimirlem16  34056  poimirlem19  34059  poimirlem23  34063  poimirlem24  34064  poimirlem25  34065  poimirlem26  34066  poimirlem27  34067  mbfposadd  34087  cnambfre  34088  itg2addnclem2  34092  fdc  34170  heibor1  34238  rrncmslem  34260  rrnheibor  34265  opidonOLD  34280  issmgrpOLD  34291  ismndo  34300  isrngo  34325  isdivrngo  34378  isfldidl2  34497  isdmn3  34502  releleccnv  34661  releccnveq  34662  brcnvep  34669  elecres  34679  eleccnvep  34683  ideq2  34712  extid  34715  relcnveq3  34725  eqres  34741  brrabga  34742  ecin0  34750  alrmomodm  34757  brxrn  34769  brxrn2  34770  elecxrn  34781  br1cnvxrn2  34787  elec1cnvxrn2  34788  br1cossinres  34830  br1cossxrnres  34831  eldmcoss  34841  elrels2  34869  elrelscnveq3  34874  br1cnvssrres  34888  brcnvssr  34889  dfrefrels2  34896  dfcnvrefrels2  34909  dfsymrels2  34924  elrefsymrelsrel  34950  dftrrels2  34954  prtlem13  35027  prter3  35041  lrelat  35173  islshpat  35176  lshpsmreu  35268  lkrpssN  35322  cmtvalN  35370  omllaw2N  35403  cvrval  35428  cvrval2  35433  cvlsupr3  35503  3dim0  35616  islln2  35670  islpln5  35694  islpln2  35695  islpln2ah  35708  islvol5  35738  islvol2  35739  4atlem11  35768  pmapglbx  35928  cdleme18d  36454  cdlemefrs29bpre0  36555  cdlemb3  36765  cdlemg33b  36866  cdlemkid3N  37092  cdlemkid4  37093  dvhb1dimN  37145  dia11N  37207  cdlemm10N  37277  dib11N  37319  dib1dim  37324  dibglbN  37325  diblsmopel  37330  dihopelvalcpre  37407  dih11  37424  dihmeetlem4preN  37465  dihmeetlem13N  37478  lcfrvalsnN  37700  lcfrlem9  37709  lcf1o  37710  mapdval4N  37791  baerlem3lem2  37869  baerlem5alem2  37870  baerlem5blem2  37871  hdmap1fval  37955  hdmapfval  37986  hdmapglem7a  38086  hlhillcs  38117  addsubeq4com  38152  prjspreln0  38217  ellz1  38300  lzunuz  38301  fz1eqin  38302  diophrex  38309  rexrabdioph  38328  rexfrabdioph  38329  2rexfrabdioph  38330  3rexfrabdioph  38331  4rexfrabdioph  38332  6rexfrabdioph  38333  7rexfrabdioph  38334  fzneg  38518  expdioph  38559  wepwsolem  38581  fnwe2lem2  38590  islmodfg  38608  kercvrlsm  38622  sdrgacs  38740  cnvcnvintabd  38873  iunrelexpuztr  38978  brtrclfv2  38986  frege124d  39020  rcompleq  39284  or3or  39285  uneqsn  39287  clsk1independent  39310  ntrclsneine0lem  39328  ntrclsiso  39331  ntrclsk2  39332  ntrclskb  39333  ntrclsk3  39334  ntrclsk13  39335  ntrclsk4  39336  ntrneiel2  39350  ntrneiiso  39355  ntrneikb  39358  ntrneik3  39360  ntrneix3  39361  ntrneik13  39362  ntrneix13  39363  ntrneik4w  39364  k0004lem3  39413  pm10.52  39530  iotasbc  39585  pm14.122a  39588  pm14.122b  39589  pm14.123a  39591  rusbcALT  39605  fvsb  39620  trsbc  39710  iunxsngf2  40171  limcperiod  40778  limsupre  40791  dvbdfbdioo  41083  stoweidlem34  41188  fourierdlem108  41368  fourierdlem110  41370  etransc  41437  funressnfv  42117  2reu4a  42160  dfafn5a  42211  ndfatafv2nrn  42272  afv2ndefb  42275  dfatsnafv2  42303  dfatdmfcoafv2  42305  dfatco  42307  afv2fv0xorb  42318  readdcnnred  42355  resubcnnred  42356  recnmulnred  42357  cndivrenred  42358  elfz2z  42367  el1fzopredsuc  42377  iccelpart  42411  lighneallem2  42554  dfeven2  42597  gbowge7  42686  sbgoldbwt  42700  isupwlk  42769  uspgrsprfo  42781  ismhm0  42830  inclfusubc  42892  isrnghm  42917  rnghmval2  42920  uzlidlring  42954  lidldomnnring  42955  zrninitoringc  43096  opeliun2xp  43136  snlindsntor  43285  elbigo2  43371  resum2sqorgt0  43455  rrx2pnedifcoorneor  43462  rrx2plord  43466  rrx2plordisom  43469  eenglngeehlnmlem1  43483  eenglngeehlnmlem2  43484  rrx2linest2  43490  itsclc0b  43518  itsclinecirc0in  43521  inlinecirc02plem  43532  gte-lte  43583  gt-lt  43584
  Copyright terms: Public domain W3C validator