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

Theorem syl5bb 271
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 267 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  syl5rbb  272  syl5bbr  273  3bitr4g  302  imim21b  381  ifpfal  1018  cad0  1547  ax12wdemo  1999  sbal2  2449  necon3abid  2818  necon3bid  2826  ralxpxfr2d  3298  ceqsrexv  3306  ceqsrex2v  3308  elab2g  3322  elrabf  3329  elrab3t  3330  eueq2  3347  eqreu  3365  reu8  3369  ru  3401  sbcralt  3477  sbcabel  3483  sbcel1g  3939  sbcel2  3941  csbnestgf  3948  sbccsb2  3957  disjpss  3980  sbcssg  4035  rexsng  4166  ralprg  4181  rexprg  4182  difsn  4269  preq2b  4318  opthpr  4324  preqsnd  4330  csbopg  4358  ralunsn  4360  csbuni  4402  dfiin2g  4489  iunxsng  4538  elpwuni  4549  disjxun  4581  sbcbr12g  4638  pwnss  4756  opthneg  4876  otthg  4880  opelopabt  4912  opelopabga  4913  brabga  4914  opelopabgf  4920  csbmpt12  4934  rbropapd  4939  dfid3  4954  frirr  5015  wereu2  5035  brab2a  5091  opeliunxp  5093  posn  5110  sosn  5111  frsn  5112  brab2ga  5117  opbrop  5121  csbcnvgALT  5229  elrnmpt1  5295  elrnmptg  5296  eliniseg2  5424  poleloe  5446  xpdifid  5481  cnvpo  5590  elpred  5610  ordtri4  5678  oneqmini  5693  elsucg  5709  elsuc2g  5710  sbcfung  5827  dffun8  5831  fncnv  5876  fununi  5878  fnssresb  5917  fnimaeq0  5926  csbfv12  6141  dffn5  6151  funimass4  6157  feqmptdf  6161  fnsnfv  6168  dmfco  6182  fndmdif  6229  fvimacnvi  6239  fvimacnvALT  6244  unpreima  6249  respreima  6252  fmptco  6303  fressnfv  6332  fmptsnd  6340  fnnfpeq0  6349  tpres  6371  elunirn  6413  dff13  6416  f12dfv  6429  f13dfv  6430  fliftel  6459  isoini  6488  f1oiso  6501  eloprabga  6645  resoprab2  6655  elrnmpt2res  6672  ralrnmpt2  6673  ovid  6675  ov  6678  ovg  6697  ofrfval2  6813  dfwe2  6873  ssonprc  6884  ordpwsuc  6907  dfom2  6959  f1oweALT  7043  el2xptp0  7103  fmpt2x  7125  ovmptss  7145  1stconst  7152  2ndconst  7153  fnsuppres  7209  brtpos2  7245  mpt2curryd  7282  dfsmo2  7331  rdglim2  7415  seqomlem2  7433  omeu  7552  oeeui  7569  brdifun  7658  eqerlem  7663  brecop  7727  erovlem  7730  eceqoveq  7740  mapsn  7785  ixpsnval  7797  mptelixpg  7831  map1  7921  xpsnen  7929  xpdom2  7940  omxpenlem  7946  xpf1o  8007  mapunen  8014  onfin  8036  fimaxg  8092  fodomfib  8125  fofinf1o  8126  fipreima  8155  supub  8248  infglb  8279  infglbb  8280  fiming  8287  fiinfg  8288  ordtypecbv  8305  ordtypelem3  8308  ordtypelem9  8314  hartogslem1  8330  wofib  8333  wemapsolem  8338  wemapso2lem  8340  noinfep  8440  cantnf  8473  rankbnd2  8615  domtri2  8698  infxpenc2  8728  fseqdom  8732  acni2  8752  dfac9  8841  cfeq0  8961  cfsuc  8962  cflim3  8967  cfslb  8971  cofsmo  8974  enfin2i  9026  isfin3ds  9034  isf33lem  9071  fin1a2lem5  9109  axdc2lem  9153  zorn2g  9208  fodomb  9229  brdom7disj  9234  brdom6disj  9235  iundom2g  9241  cfpwsdom  9285  elgch  9323  fpwwe2cbv  9331  fpwwecbv  9345  pwfseqlem3  9361  pwfseqlem4a  9362  pwfseqlem4  9363  ltpiord  9588  nlt1pi  9607  nqereu  9630  addclprlem1  9717  1idpr  9730  reclem3pr  9750  ltsosr  9794  map2psrpr  9810  supsrlem  9811  axrrecex  9863  xrlenlt  9982  eqlei2  10027  addsubeq4  10175  renegcli  10221  lesub0  10424  wloglei  10439  conjmul  10621  rereccl  10622  infm3  10861  supaddc  10867  supadd  10868  supmul1  10869  supmullem1  10870  supmullem2  10871  supmul  10872  creui  10892  nndiv  10938  elznn0  11269  prime  11334  eqreznegel  11650  zsupss  11653  rebtwnz  11663  negelrp  11740  ltxr  11825  elixx3g  12059  ixxun  12062  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  difreicc  12175  divelunit  12185  iccf1o  12187  elfz2  12204  fzn  12228  fznn  12278  fzshftral  12297  nelfzo  12344  fzosplitsni  12444  om2uzisoi  12615  rabssnn0fi  12647  mptnn0fsupp  12659  sq11i  12816  hashsdom  13031  fi1uzind  13134  fi1uzindOLD  13140  wrdval  13163  csbwrdg  13189  wrd2ind  13329  s2f1o  13511  cjreb  13711  rexfiuz  13935  cau3lem  13942  rlim2  14075  ello12  14095  ello1mpt  14100  elo12  14106  o1lo1  14116  lo1resb  14143  o1resb  14145  o1compt  14166  caucvgb  14258  pwm1geoser  14439  mertens  14457  ruclem12  14809  divides  14823  dvdsabseq  14873  odd2np1  14903  oddm1even  14905  sumodd  14949  divalgmod  14967  modremain  14970  sadadd2lem2  15010  gcdcllem2  15060  bezoutlem2  15095  bezoutlem3  15096  bezoutlem4  15097  isprm2  15233  isprm3  15234  dvdsnprmd  15241  oddprmdvds  15445  prmreclem2  15459  prmreclem5  15462  prmreclem6  15463  4sqlem2  15491  4sqlem12  15498  vdwmc  15520  vdwpc  15522  vdwlem6  15528  vdwlem10  15532  vdwnn  15540  ramval  15550  0ram  15562  prdsleval  15960  pwsle  15975  imasleval  16024  xpsfrnel2  16048  xpsle  16064  isacs2  16137  mreacs  16142  acsfn  16143  iscatd2  16165  catpropd  16192  ciclcl  16285  cicrcl  16286  isssc  16303  evlfcl  16685  uncfcurf  16702  pltval  16783  lublecllem  16811  tosso  16859  oduleg  16955  oduclatb  16967  posglbmo  16970  isipodrs  16984  odudlatb  17019  gsumvalx  17093  sgrp2rid2  17236  grplmulf1o  17312  grplactcnv  17341  elnmz  17456  eqgid  17469  isghm  17483  ghmeqker  17510  resscntz  17587  symg1bas  17639  pgrpsubgsymgbi  17650  symgfixelq  17676  f1omvdconj  17689  odmulgeq  17797  sylow3lem3  17867  sylow3lem6  17870  efgval2  17960  efgsdm  17966  efgrelexlema  17985  efgcpbllemb  17991  iscyggen2  18106  cyggenod  18109  gsummptfzcl  18191  eldprd  18226  dprdf11  18245  dprddisj2  18261  pgpfac1lem2  18297  pgpfac1  18302  srg1zr  18352  drngid2  18586  issubrg  18603  islmod  18690  aspval2  19168  psrbag  19185  cply1coe0bi  19491  zndvds  19717  znleval  19722  iunocv  19844  pjfval2  19872  pjdm2  19874  dsmmelbas  19902  ellspd  19960  islindf  19970  islindf4  19996  istopg  20525  basgen2  20604  isclo  20701  mretopd  20706  isnei  20717  isperf3  20767  restdis  20792  neitr  20794  restcls  20795  restlp  20797  restperf  20798  iscn  20849  iscnp  20851  lmbr2  20873  lmbrf  20874  ordtt1  20993  cmpsub  21013  hauscmplem  21019  cmpfi  21021  dfcon2  21032  1stcelcls  21074  1stccn  21076  nllyi  21088  subislly  21094  dissnlocfin  21142  elkgen  21149  ptpjpre1  21184  ptuni2  21189  ptclsg  21228  ptcnplem  21234  txcn  21239  hausdiag  21258  txhaus  21260  txkgen  21265  xkoptsub  21267  cnmpt21  21284  elqtop  21310  tgqtop  21325  r0cld  21351  elfg  21485  fbasrn  21498  trfil2  21501  trfil3  21502  fin1aufil  21546  elfm2  21562  elfm3  21564  flimopn  21589  fbflim  21590  flfnei  21605  flftg  21610  cnpflf2  21614  txflf  21620  fclsbas  21635  alexsubALTlem4  21664  cnextfvval  21679  snclseqg  21729  tgphaus  21730  tsmsfbas  21741  tsmssubm  21756  utopsnneip  21862  prdsxmetlem  21983  imasdsf1olem  21988  xpsdsval  21996  blres  22046  isxms2  22063  metcnp  22156  txmetcnp  22162  txmetcn  22163  metustel  22165  metuel2  22180  dscopn  22188  isngp4  22226  cnblcld  22388  metnrmlem1a  22469  icoopnst  22546  iocopnst  22547  elpi1  22653  isclmp  22705  isncvsngp  22757  lmmbr2  22865  cfil3i  22875  caucfil  22889  iscmet3  22899  lmclim  22909  metcld2  22913  bcthlem4  22932  minveclem3b  23007  minveclem6  23013  minveclem7  23014  ivthle  23032  ivthle2  23033  evthicc2  23036  ovolfioo  23043  ovolficc  23044  ovolgelb  23055  dyadmax  23172  subopnmbl  23178  ismbf3d  23227  mbfimaopnlem  23228  mbfimaopn2  23230  mbfaddlem  23233  mbfsup  23237  mbfinf  23238  i1f1lem  23262  i1fmulclem  23275  itg1climres  23287  mbfi1fseqlem4  23291  itg2monolem1  23323  itg2gt0  23333  isibl  23338  iblcnlem1  23360  ellimc2  23447  dvcnvrelem1  23584  itgsubst  23616  mdegleb  23628  fta1glem2  23730  quotval  23851  vieta1lem1  23869  vieta1lem2  23870  ulm2  23943  ulmcaulem  23952  ulmcau  23953  radcnvlt1  23976  sineq0  24077  cos11  24083  recosf1o  24085  efopn  24204  cxpeq  24298  mcubic  24374  birthdaylem3  24480  rlimcnp  24492  xrlimcnp  24495  eldmgm  24548  dmgmaddn0  24549  lgamgulmlem6  24560  wilth  24597  isppw  24640  isppw2  24641  mumullem2  24706  sqff1o  24708  dvdsmulf1o  24720  fsumvma  24738  fsumvma2  24739  vmasum  24741  chpchtsum  24744  lgsne0  24860  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1a  24916  dchrmusumlema  24982  rpvmasum2  25001  dchrisum0lema  25003  pntibndlem3  25081  pntlemi  25093  pntleml  25100  pnt3  25101  trgcgrg  25210  tgcgr4  25226  colcom  25253  colrot1  25254  ltgov  25292  hlcomb  25298  lncom  25317  mirreu3  25349  isperp  25407  perpcom  25408  brbtwn  25579  brcgr  25580  brbtwn2  25585  colinearalg  25590  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  isuhgr  25726  isushgr  25727  isupgr  25751  isumgr  25761  nbgraf1olem1  25970  nbgraf1olem5  25974  nbcusgra  25992  uvtx01vtx  26020  cusgrauvtxb  26024  iswlk  26048  istrl  26067  ispth  26098  isspth  26099  wlkdvspthlem  26137  usgrcyclnl2  26169  wwlkn0s  26233  wwlkextwrd  26256  wwlkextproplem3  26271  isclwlk0  26282  clwwlkn2  26303  eclclwwlkn1  26359  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkfclwwlk1hashn  26368  clwlkfoclwwlk  26372  usg2spthonot  26415  isrgra  26453  isrusgra  26454  isrusgusrg  26459  eupath2  26507  frgra3vlem2  26528  frgrancvvdeqlem2  26558  frgrancvvdeqlem3  26559  frgrancvvdeqlemC  26566  usg2spot2nb  26592  isvclem  26816  isnvlem  26849  isphg  27056  isph  27061  phoeqi  27097  ubthlem3  27112  minvecolem5  27121  minvecolem6  27122  minvecolem7  27123  hhph  27419  issh3  27460  nmopub  28151  nmfnleub  28168  adjeq  28178  adjvalval  28180  elunop2  28256  lnophm  28262  nmcexi  28269  cnlnadjlem5  28314  cnlnadjeui  28320  adjbd1o  28328  jpi  28513  mddmd2  28552  chrelati  28607  chrelat2i  28608  cvexchlem  28611  dmdbr5ati  28665  cdjreui  28675  cdj3i  28684  iunxsngf  28758  disjunsn  28789  opeldifid  28794  fcoinvbr  28799  brabgaf  28800  opabdm  28803  opabrn  28804  iunsnima  28808  abfmpunirn  28832  fmptcof2  28839  funcnvmptOLD  28850  funcnvmpt  28851  funcnv5mpt  28852  f1od2  28887  resf1o  28893  fpwrelmap  28896  iocinioc2  28931  eliccioo  28970  posrasymb  28988  isslmd  29086  smatrcl  29190  pstmxmet  29268  prsdm  29288  prsrn  29289  ordtconlem1  29298  xrmulc1cn  29304  ispisys2  29543  elcarsg  29694  eulerpartlemmf  29764  isrrvv  29832  bnj976  30102  bnj944  30262  bnj1173  30324  bnj1321  30349  bnj1373  30352  bnj1417  30363  subfacp1lem3  30418  subfacp1lem6  30421  subfacp1  30422  txpcon  30468  sconpi1  30475  rescon  30482  cvmscbv  30494  cvmsval  30502  cvmlift2lem13  30551  cvmlift3lem2  30556  cvmlift3  30564  mclsrcl  30712  br8  30899  br6  30900  br4  30901  fv1stcnv  30925  fv2ndcnv  30926  distel  30953  poseq  30994  wsuclem  31017  wsuclemOLD  31018  sltsolem1  31067  imageval  31207  funpartfv  31222  dfrdg4  31228  altopthg  31244  altopthbg  31245  brcolinear2  31335  lineext  31353  brsegle  31385  seglelin  31393  broutsideof2  31399  isfne4  31505  isfne2  31507  isfne3  31508  fneval  31517  topfneec  31520  neibastop2lem  31525  neibastop2  31526  neifg  31536  filnetlem4  31546  onsuct0  31610  bj-abbi  31963  bj-tagcg  32166  bj-projval  32177  bj-restuni  32231  csbwrecsg  32349  csboprabg  32352  csbmpt22g  32353  topdifinffinlem  32371  isbasisrelowllem1  32379  isbasisrelowllem2  32380  rdgeqoa  32394  csbfinxpg  32401  wl-sbrimt  32510  wl-sblimt  32511  wl-sbnf1  32515  wl-mo2df  32531  wl-eudf  32533  wl-mo2t  32536  wl-mo3t  32537  wl-ax11-lem6  32546  uncov  32560  tan2h  32571  matunitlindf  32577  ptrest  32578  poimirlem2  32581  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  mbfposadd  32627  cnambfre  32628  itg2addnclem2  32632  fdc  32711  heibor1  32779  rrncmslem  32801  rrnheibor  32806  opidonOLD  32821  issmgrpOLD  32832  ismndo  32841  isrngo  32866  isdivrngo  32919  isfldidl2  33038  isdmn3  33043  prtlem13  33171  prter3  33185  lrelat  33319  islshpat  33322  lshpsmreu  33414  lkrpssN  33468  cmtvalN  33516  omllaw2N  33549  cvrval  33574  cvrval2  33579  cvlsupr3  33649  3dim0  33761  islln2  33815  islpln5  33839  islpln2  33840  islpln2ah  33853  islvol5  33883  islvol2  33884  4atlem11  33913  pmapglbx  34073  cdleme18d  34600  cdlemefrs29bpre0  34702  cdlemb3  34912  cdlemg33b  35013  cdlemkid3N  35239  cdlemkid4  35240  dvhb1dimN  35292  dia11N  35355  cdlemm10N  35425  dib11N  35467  dib1dim  35472  dibglbN  35473  diblsmopel  35478  dihopelvalcpre  35555  dih11  35572  dihmeetlem4preN  35613  dihmeetlem13N  35626  lcfrvalsnN  35848  lcfrlem9  35857  lcf1o  35858  mapdval4N  35939  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  hdmap1fval  36104  hdmapfval  36137  hdmapglem7a  36237  hlhillcs  36268  ellz1  36348  lzunuz  36349  fz1eqin  36350  diophrex  36357  rexrabdioph  36376  rexfrabdioph  36377  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  fzneg  36567  expdioph  36608  wepwsolem  36630  fnwe2lem2  36639  islmodfg  36657  kercvrlsm  36671  sdrgacs  36790  cnvcnvintabd  36925  iunrelexpuztr  37030  brtrclfv2  37038  frege124d  37072  rcompleq  37338  or3or  37339  uneqsn  37341  clsk1independent  37364  ntrclsneine0lem  37382  ntrclsiso  37385  ntrclsk2  37386  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrclsk4  37390  ntrneiel2  37404  ntrneiiso  37409  ntrneikb  37412  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  ntrneik4w  37418  k0004lem3  37467  pm10.52  37586  iotasbc  37642  pm14.122a  37645  pm14.122b  37646  pm14.123a  37648  rusbcALT  37662  fvsb  37677  trsbc  37771  rexsngf  38245  iunxsngf2  38255  mapsnd  38383  limcperiod  38695  limsupre  38708  dvbdfbdioo  38820  stoweidlem34  38927  fourierdlem108  39107  fourierdlem110  39109  etransc  39176  2reu4a  39838  funressnfv  39857  dfafn5a  39889  el1fzopredsuc  39948  iccelpart  39971  lighneallem2  40061  dfeven2  40100  gboge7  40185  bgoldbwt  40199  riotaeqimp  40338  elfz2z  40352  isuspgr  40382  isusgr  40383  uhgr0v0e  40464  isfusgrf1  40539  opfusgr  40542  usgr1v0e  40545  nbuhgr2vtx1edgb  40574  edgnbusgreu  40595  nbusgredgeu0  40596  isuvtxa  40621  cusgruvtxb  40644  cplgr3v  40657  cusgrsizeinds  40668  vtxdg0v  40688  vtxd0nedgb  40703  vtxduhgr0nedg  40707  vtxdusgr0edgnelALT  40711  is1wlk  40813  isWlk  40814  1wlk1walk  40843  upgr2wlk  40876  usgr2pthlem  40969  isclWlke  40984  isclWlkupgr  40985  iswwlksnx  41042  wwlksnextwrd  41103  wwlksnextproplem3  41117  umgr2wlk  41156  elwwlks2  41170  elwspths2spth  41171  clwlkclwwlk  41211  clwwlksn2  41217  eclclwwlksn1  41259  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk1hashn  41266  clwlksfoclwwlk  41270  clwwlksnun  41281  1pthon2v-av  41320  uhgr3cyclex  41349  isconngr  41356  isconngr1  41357  eupth2lems  41406  isfrgr  41430  frgr0v  41433  frgr3vlem2  41444  frgrncvvdeqlem2  41470  frgrncvvdeqlem3  41471  frgrncvvdeqlemC  41478  fusgr2wsp2nb  41498  ismhm0  41595  inclfusubc  41657  isrnghm  41682  rnghmval2  41685  uzlidlring  41719  lidldomnnring  41720  zrninitoringc  41863  opeliun2xp  41904  snlindsntor  42054  elbigo2  42144  setrec1lem1  42233  gte-lte  42264  gt-lt  42265
  Copyright terms: Public domain W3C validator