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

Theorem syl5bb 272
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 268 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  syl5rbb  273  syl5bbr  274  3bitr4g  303  imim21b  381  ifpfal  1061  cad0  1704  ax12wdemo  2167  sbal2  2609  necon3abid  2979  necon3bid  2987  ralxpxfr2d  3478  ceqsrexv  3487  ceqsrex2v  3489  elab2g  3505  elrabf  3512  elrab3t  3515  eueq2  3533  eqreu  3551  reu8  3555  ru  3587  sbcralt  3661  sbcabel  3667  sbcel1g  4132  sbcel2  4134  csbnestgf  4141  sbccsb2  4150  disjpss  4172  sbcssg  4225  rexsng  4358  ralprg  4372  rexprg  4373  difsn  4465  preq2b  4511  opthpr  4516  preqsnd  4524  preqsndOLD  4525  csbopg  4558  ralunsn  4561  csbuni  4603  dfiin2g  4688  iunxsng  4737  elpwuni  4751  disjxun  4785  sbcbr12g  4843  pwnss  4962  opthneg  5078  otthg  5082  opeqsng  5095  snopeqop  5099  opelopabt  5121  opelopabga  5122  brabga  5123  opelopabgf  5129  csbmpt12  5144  rbropapd  5149  dfid3  5159  frirr  5227  wereu2  5247  opeliunxp  5311  posn  5328  sosn  5329  frsn  5330  brab2a  5335  opbrop  5339  csbcnvgALT  5446  elrnmpt1  5513  elrnmptg  5514  opelresg  5541  eliniseg2  5647  poleloe  5669  xpdifid  5704  cnvpo  5818  elpred  5837  ordtri4  5905  oneqmini  5920  elsucg  5936  elsuc2g  5937  sbcfung  6056  dffun8  6060  fncnv  6103  fununi  6105  fnssresb  6144  fnimaeq0  6154  csbfv12  6373  dffn5  6384  funimass4  6390  feqmptdf  6394  fnsnfv  6401  dmfco  6415  fndmdif  6465  fvimacnvi  6475  fvimacnvALT  6480  unpreima  6485  respreima  6488  fmptco  6540  fressnfv  6571  fmptsnd  6580  fnnfpeq0  6589  tpres  6611  elunirn  6653  dff13  6656  f12dfv  6673  f13dfv  6674  fliftel  6703  isoini  6732  f1oiso  6745  riotaeqimp  6778  fnbrovb  6840  eloprabga  6895  resoprab2  6905  elrnmpt2res  6922  ralrnmpt2  6923  ovid  6925  ov  6928  ovg  6947  ofrfval2  7063  dfwe2  7129  ssonprc  7140  ordpwsuc  7163  dfom2  7215  f1oweALT  7300  el2xptp0  7362  fmpt2x  7387  ovmptss  7410  1stconst  7417  2ndconst  7418  fnsuppres  7475  brtpos2  7511  mpt2curryd  7548  dfsmo2  7598  rdglim2  7682  seqomlem2  7700  omeu  7820  oeeui  7837  brdifun  7926  eqerlem  7931  brecop  7993  erovlem  7997  eceqoveq  8006  mapsnd  8052  ixpsnval  8066  mptelixpg  8100  xpsnen  8201  xpdom2  8212  omxpenlem  8218  xpf1o  8279  mapunen  8286  onfin  8308  fimaxg  8364  fodomfib  8397  fofinf1o  8398  fipreima  8429  supub  8522  infglb  8553  infglbb  8554  fiming  8561  fiinfg  8562  ordtypecbv  8579  ordtypelem3  8582  ordtypelem9  8588  hartogslem1  8604  wofib  8607  wemapsolem  8612  wemapso2lem  8614  noinfep  8722  cantnf  8755  rankbnd2  8897  domtri2  9016  infxpenc2  9046  fseqdom  9050  acni2  9070  dfac9  9161  cfeq0  9281  cfsuc  9282  cflim3  9287  cfslb  9291  cofsmo  9294  enfin2i  9346  isfin3ds  9354  isf33lem  9391  fin1a2lem5  9429  axdc2lem  9473  zorn2g  9528  fodomb  9551  brdom7disj  9556  brdom6disj  9557  iundom2g  9565  cfpwsdom  9609  elgch  9647  fpwwe2cbv  9655  fpwwecbv  9669  pwfseqlem3  9685  pwfseqlem4a  9686  pwfseqlem4  9687  ltpiord  9912  nlt1pi  9931  nqereu  9954  addclprlem1  10041  1idpr  10054  reclem3pr  10074  ltsosr  10118  map2psrpr  10134  supsrlem  10135  axrrecex  10187  xrlenlt  10306  eqlei2  10351  addsubeq4  10499  renegcli  10545  lesub0  10748  wloglei  10763  conjmul  10945  rereccl  10946  infm3  11185  supaddc  11193  supadd  11194  supmul1  11195  supmullem1  11196  supmullem2  11197  supmul  11198  creui  11218  nndiv  11264  elznn0  11595  prime  11661  eqreznegel  11978  zsupss  11981  rebtwnz  11991  negelrp  12068  ltxr  12155  elixx3g  12394  ixxun  12397  ioo0  12406  ico0  12427  ioc0  12428  icc0  12429  difreicc  12512  divelunit  12522  iccf1o  12524  elfz2  12541  fzn  12565  fznn  12616  fzshftral  12636  nelfzo  12684  fzosplitsni  12788  om2uzisoi  12962  rabssnn0fi  12994  mptnn0fsupp  13005  sq11i  13162  hashsdom  13373  fi1uzind  13482  wrdval  13505  csbwrdg  13531  wrd2ind  13687  s2f1o  13871  cjreb  14072  rexfiuz  14296  cau3lem  14303  rlim2  14436  ello12  14456  ello1mpt  14461  elo12  14467  o1lo1  14477  lo1resb  14504  o1resb  14506  o1compt  14527  caucvgb  14619  pwm1geoser  14808  mertens  14826  ruclem12  15177  divides  15192  dvdsabseq  15245  odd2np1  15274  oddm1even  15276  sumodd  15320  divalgmod  15338  modremain  15341  sadadd2lem2  15381  gcdcllem2  15431  bezoutlem2  15466  bezoutlem3  15467  bezoutlem4  15468  isprm2  15603  isprm3  15604  dvdsnprmd  15611  oddprmdvds  15815  prmreclem2  15829  prmreclem5  15832  prmreclem6  15833  4sqlem2  15861  4sqlem12  15868  vdwmc  15890  vdwpc  15892  vdwlem6  15898  vdwlem10  15902  vdwnn  15910  ramval  15920  0ram  15932  prdsleval  16346  pwsle  16361  imasleval  16410  xpsfrnel2  16434  xpsle  16450  isacs2  16522  mreacs  16527  acsfn  16528  iscatd2  16550  catpropd  16577  ciclcl  16670  cicrcl  16671  isssc  16688  evlfcl  17071  uncfcurf  17088  pltval  17169  lublecllem  17197  tosso  17245  oduleg  17341  oduclatb  17353  posglbmo  17356  isipodrs  17370  odudlatb  17405  gsumvalx  17479  sgrp2rid2  17622  grplmulf1o  17698  grplactcnv  17727  elnmz  17842  eqgid  17855  isghm  17869  ghmeqker  17896  resscntz  17972  symg1bas  18024  pgrpsubgsymgbi  18035  symgfixelq  18061  f1omvdconj  18074  odmulgeq  18182  sylow3lem3  18252  sylow3lem6  18255  efgval2  18345  efgsdm  18351  efgrelexlema  18370  efgcpbllemb  18376  iscyggen2  18491  cyggenod  18494  gsummptfzcl  18576  eldprd  18612  dprdf11  18631  dprddisj2  18647  pgpfac1lem2  18683  pgpfac1  18688  srg1zr  18738  drngid2  18974  issubrg  18991  islmod  19078  aspval2  19563  psrbag  19580  cply1coe0bi  19886  zndvds  20114  znleval  20119  iunocv  20243  pjfval2  20271  pjdm2  20273  dsmmelbas  20301  ellspd  20359  islindf  20369  islindf4  20395  istopg  20921  basgen2  21015  isclo  21113  mretopd  21118  isnei  21129  isperf3  21179  restdis  21204  neitr  21206  restcls  21207  restlp  21209  restperf  21210  iscn  21261  iscnp  21263  lmbr2  21285  lmbrf  21286  ordtt1  21405  cmpsub  21425  hauscmplem  21431  cmpfi  21433  dfconn2  21444  1stcelcls  21486  1stccn  21488  nllyi  21500  subislly  21506  dissnlocfin  21554  elkgen  21561  ptpjpre1  21596  ptuni2  21601  ptclsg  21640  ptcnplem  21646  txcn  21651  hausdiag  21670  txhaus  21672  txkgen  21677  xkoptsub  21679  cnmpt21  21696  elqtop  21722  tgqtop  21737  r0cld  21763  elfg  21896  fbasrn  21909  trfil2  21912  trfil3  21913  fin1aufil  21957  elfm2  21973  elfm3  21975  flimopn  22000  fbflim  22001  flfnei  22016  flftg  22021  cnpflf2  22025  txflf  22031  fclsbas  22046  alexsubALTlem4  22075  cnextfvval  22090  snclseqg  22140  tgphaus  22141  tsmsfbas  22152  tsmssubm  22167  utopsnneip  22273  prdsxmetlem  22394  imasdsf1olem  22399  xpsdsval  22407  blres  22457  isxms2  22474  metcnp  22567  txmetcnp  22573  txmetcn  22574  metustel  22576  metuel2  22591  dscopn  22599  isngp4  22637  cnblcld  22799  metnrmlem1a  22882  icoopnst  22959  iocopnst  22960  elpi1  23065  isclmp  23117  isncvsngp  23169  lmmbr2  23277  cfil3i  23287  caucfil  23301  iscmet3  23311  lmclim  23321  metcld2  23325  bcthlem4  23344  minveclem3b  23419  minveclem6  23425  minveclem7  23426  ivthle  23445  ivthle2  23446  evthicc2  23449  ovolfioo  23456  ovolficc  23457  ovolgelb  23469  dyadmax  23587  subopnmbl  23593  ismbf3d  23642  mbfimaopnlem  23643  mbfimaopn2  23645  mbfaddlem  23648  mbfsup  23652  mbfinf  23653  i1f1lem  23677  i1fmulclem  23690  itg1climres  23702  mbfi1fseqlem4  23706  itg2monolem1  23738  itg2gt0  23748  isibl  23753  iblcnlem1  23775  ellimc2  23862  dvcnvrelem1  24001  itgsubst  24033  mdegleb  24045  fta1glem2  24147  quotval  24268  vieta1lem1  24286  vieta1lem2  24287  ulm2  24360  ulmcaulem  24369  ulmcau  24370  radcnvlt1  24393  sineq0  24495  cos11  24501  recosf1o  24503  efopn  24626  cxpeq  24720  mcubic  24796  birthdaylem3  24902  rlimcnp  24914  xrlimcnp  24917  eldmgm  24970  dmgmaddn0  24971  lgamgulmlem6  24982  wilth  25019  isppw  25062  isppw2  25063  mumullem2  25128  sqff1o  25130  dvdsmulf1o  25142  fsumvma  25160  fsumvma2  25161  vmasum  25163  chpchtsum  25166  lgsne0  25282  gausslemma2dlem0i  25311  gausslemma2dlem1a  25312  lgseisenlem2  25323  lgsquadlem1  25327  lgsquadlem2  25328  2lgslem1a  25338  dchrmusumlema  25404  rpvmasum2  25423  dchrisum0lema  25425  pntibndlem3  25503  pntlemi  25515  pntleml  25522  pnt3  25523  trgcgrg  25632  tgcgr4  25648  colcom  25675  colrot1  25676  ltgov  25714  hlcomb  25720  lncom  25739  mirreu3  25771  isperp  25829  perpcom  25830  brbtwn  26001  brcgr  26002  brbtwn2  26007  colinearalg  26012  axeuclidlem  26064  axcontlem2  26067  axcontlem4  26069  axcontlem7  26072  edgiedgb  26169  isuhgr  26177  isushgr  26178  isupgr  26201  isumgr  26212  isuspgr  26270  isusgr  26271  uhgr0v0e  26354  isfusgrf1  26436  opfusgr  26439  usgr1v0e  26442  dfnbgr3  26455  nbuhgr2vtx1edgb  26472  edgnbusgreu  26492  edgnbusgreuOLD  26493  nbusgredgeu0  26494  isuvtx  26523  isuvtxaOLD  26524  cusgruvtxb  26554  cplgr3v  26567  cusgrsizeinds  26584  vtxdg0v  26605  vtxd0nedgb  26620  vtxduhgr0nedg  26624  vtxdusgr0edgnelALT  26628  iswlk  26742  wlk1walk  26771  upgr2wlk  26800  upgristrl  26835  2pthnloop  26863  usgr2pthlem  26895  isclwlke  26909  isclwlkupgr  26910  iswwlksnx  26969  wwlksnextwrd  27042  wwlksnextproplem3  27057  2pthon3v  27091  umgr2wlk  27097  elwwlks2on  27108  elwwlks2  27116  elwspths2spth  27117  clwwlknclwwlkdif  27128  clwlkclwwlk  27153  clwwlkn1  27198  clwwlkn2  27201  eclclwwlkn1  27234  eleclclwwlkn  27235  hashecclwwlkn1  27236  umgrhashecclwwlk  27237  clwlksfclwwlk1hashnOLD  27241  clwlksfoclwwlkOLD  27245  clwwlknonel  27270  clwwlknon1  27273  clwwlknun  27289  clwwlknunOLD  27294  1pthon2v  27334  uhgr3cyclex  27363  isconngr  27370  isconngr1  27371  eupthres  27396  eupth2lems  27419  isfrgr  27441  frgr0v  27444  frgr3vlem2  27457  fusgr2wsp2nb  27517  extwwlkfab  27539  numclwwlk1lem2foa  27541  numclwwlk1lem2fo  27545  isvclem  27773  isnvlem  27806  isphg  28013  isph  28018  phoeqi  28054  ubthlem3  28069  minvecolem5  28078  minvecolem6  28079  minvecolem7  28080  hhph  28376  issh3  28417  nmopub  29108  nmfnleub  29125  adjeq  29135  adjvalval  29137  elunop2  29213  lnophm  29219  nmcexi  29226  cnlnadjlem5  29271  cnlnadjeui  29277  adjbd1o  29285  jpi  29470  mddmd2  29509  chrelati  29564  chrelat2i  29565  cvexchlem  29568  dmdbr5ati  29622  cdjreui  29632  cdj3i  29641  iunxsngf  29714  disjunsn  29746  opeldifid  29751  fcoinvbr  29758  brabgaf  29759  opabdm  29762  opabrn  29763  iunsnima  29769  elimampt  29779  abfmpunirn  29793  fmptcof2  29798  funcnvmptOLD  29808  funcnvmpt  29809  funcnv5mpt  29810  f1od2  29840  resf1o  29846  fpwrelmap  29849  iocinioc2  29882  eliccioo  29980  posrasymb  29998  isslmd  30096  smatrcl  30203  pstmxmet  30281  prsdm  30301  prsrn  30302  ordtconnlem1  30311  xrmulc1cn  30317  ispisys2  30557  elcarsg  30708  eulerpartlemmf  30778  isrrvv  30846  reprinrn  31037  tgoldbachgt  31082  bnj976  31187  bnj944  31347  bnj1173  31409  bnj1321  31434  bnj1373  31437  bnj1417  31448  subfacp1lem3  31503  subfacp1lem6  31506  subfacp1  31507  txpconn  31553  sconnpi1  31560  resconn  31567  cvmscbv  31579  cvmsval  31587  cvmlift2lem13  31636  cvmlift3lem2  31641  cvmlift3  31649  mclsrcl  31797  br8  31985  br6  31986  br4  31987  elintfv  32001  fv1stcnv  32017  fv2ndcnv  32018  distel  32046  frpomin  32076  poseq  32091  wsuclem  32108  sltsolem1  32164  nosupdm  32188  nosupbnd1lem4  32195  slenlt  32215  sleloe  32217  etasslt  32258  madeval2  32274  imageval  32375  funpartfv  32390  dfrdg4  32396  altopthg  32412  altopthbg  32413  brcolinear2  32503  lineext  32521  brsegle  32553  seglelin  32561  broutsideof2  32567  isfne4  32673  isfne2  32675  isfne3  32676  fneval  32685  topfneec  32688  neibastop2lem  32693  neibastop2  32694  neifg  32704  filnetlem4  32714  onsuct0  32778  bj-abbi  33112  bj-tagcg  33305  bj-projval  33316  bj-restuni  33383  bj-raldifsn  33387  csbwrecsg  33511  csboprabg  33514  csbmpt22g  33515  topdifinffinlem  33533  isbasisrelowllem1  33541  isbasisrelowllem2  33542  rdgeqoa  33556  csbfinxpg  33563  wl-sbrimt  33667  wl-sblimt  33668  wl-sbnf1  33672  wl-mo2df  33687  wl-eudf  33689  wl-mo2t  33692  wl-mo3t  33693  wl-ax11-lem6  33702  uncov  33724  tan2h  33735  matunitlindf  33741  ptrest  33742  poimirlem2  33745  poimirlem16  33759  poimirlem19  33762  poimirlem23  33766  poimirlem24  33767  poimirlem25  33768  poimirlem26  33769  poimirlem27  33770  mbfposadd  33790  cnambfre  33791  itg2addnclem2  33795  fdc  33874  heibor1  33942  rrncmslem  33964  rrnheibor  33969  opidonOLD  33984  issmgrpOLD  33995  ismndo  34004  isrngo  34029  isdivrngo  34082  isfldidl2  34201  isdmn3  34206  releleccnv  34365  releccnveq  34366  brcnvep  34373  opelresALTV  34375  elecres  34386  eleccnvep  34390  ideq2  34422  extid  34425  relcnveq3  34436  eqres  34452  ecin0  34460  alrmomodm  34467  brxrn  34479  brxrn2  34480  elecxrn  34491  br1cnvxrn2  34497  elec1cnvxrn2  34498  br1cossinres  34540  br1cossxrnres  34541  eldmcoss  34551  elrels2  34579  elrelscnveq3  34584  br1cnvssrres  34598  brcnvssr  34599  dfrefrels2  34606  dfcnvrefrels2  34619  dfsymrels2  34634  elrefsymrelsrel  34660  prtlem13  34677  prter3  34691  lrelat  34824  islshpat  34827  lshpsmreu  34919  lkrpssN  34973  cmtvalN  35021  omllaw2N  35054  cvrval  35079  cvrval2  35084  cvlsupr3  35154  3dim0  35266  islln2  35320  islpln5  35344  islpln2  35345  islpln2ah  35358  islvol5  35388  islvol2  35389  4atlem11  35418  pmapglbx  35578  cdleme18d  36105  cdlemefrs29bpre0  36206  cdlemb3  36416  cdlemg33b  36517  cdlemkid3N  36743  cdlemkid4  36744  dvhb1dimN  36796  dia11N  36859  cdlemm10N  36929  dib11N  36971  dib1dim  36976  dibglbN  36977  diblsmopel  36982  dihopelvalcpre  37059  dih11  37076  dihmeetlem4preN  37117  dihmeetlem13N  37130  lcfrvalsnN  37352  lcfrlem9  37361  lcf1o  37362  mapdval4N  37443  baerlem3lem2  37521  baerlem5alem2  37522  baerlem5blem2  37523  hdmap1fval  37607  hdmapfval  37638  hdmapglem7a  37738  hlhillcs  37769  ellz1  37857  lzunuz  37858  fz1eqin  37859  diophrex  37866  rexrabdioph  37885  rexfrabdioph  37886  2rexfrabdioph  37887  3rexfrabdioph  37888  4rexfrabdioph  37889  6rexfrabdioph  37890  7rexfrabdioph  37891  fzneg  38076  expdioph  38117  wepwsolem  38139  fnwe2lem2  38148  islmodfg  38166  kercvrlsm  38180  sdrgacs  38298  cnvcnvintabd  38433  iunrelexpuztr  38538  brtrclfv2  38546  frege124d  38580  rcompleq  38845  or3or  38846  uneqsn  38848  clsk1independent  38871  ntrclsneine0lem  38889  ntrclsiso  38892  ntrclsk2  38893  ntrclskb  38894  ntrclsk3  38895  ntrclsk13  38896  ntrclsk4  38897  ntrneiel2  38911  ntrneiiso  38916  ntrneikb  38919  ntrneik3  38921  ntrneix3  38922  ntrneik13  38923  ntrneix13  38924  ntrneik4w  38925  k0004lem3  38974  pm10.52  39091  iotasbc  39147  pm14.122a  39150  pm14.122b  39151  pm14.123a  39153  rusbcALT  39167  fvsb  39182  trsbc  39276  sbcel2gOLD  39281  sbcssOLD  39282  csbxpgOLD  39577  csbrngOLD  39580  rexsngf  39742  iunxsngf2  39752  limcperiod  40379  limsupre  40392  dvbdfbdioo  40664  stoweidlem34  40769  fourierdlem108  40949  fourierdlem110  40951  etransc  41018  2reu4a  41710  funressnfv  41729  dfafn5a  41761  elfz2z  41854  el1fzopredsuc  41864  iccelpart  41898  lighneallem2  42052  dfeven2  42091  gbowge7  42180  sbgoldbwt  42194  isupwlk  42246  uspgrsprfo  42285  ismhm0  42334  inclfusubc  42396  isrnghm  42421  rnghmval2  42424  uzlidlring  42458  lidldomnnring  42459  zrninitoringc  42600  opeliun2xp  42640  snlindsntor  42789  elbigo2  42875  gte-lte  42997  gt-lt  42998
  Copyright terms: Public domain W3C validator