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  1062  cad0  1693  ax12wdemo  2149  sbal2  2586  necon3abid  2956  necon3bid  2964  ralxpxfr2d  3454  ceqsrexv  3463  ceqsrex2v  3465  elab2g  3481  elrabf  3488  elrab3t  3491  eueq2  3509  eqreu  3527  reu8  3531  ru  3563  sbcralt  3639  sbcabel  3646  sbcel1g  4118  sbcel2  4120  csbnestgf  4127  sbccsb2  4136  disjpss  4160  sbcssg  4217  rexsng  4351  ralprg  4366  rexprg  4367  difsn  4461  preq2b  4511  opthpr  4516  preqsnd  4524  preqsndOLD  4525  csbopg  4559  ralunsn  4562  csbuni  4606  dfiin2g  4693  iunxsng  4742  elpwuni  4756  disjxun  4790  sbcbr12g  4848  pwnss  4967  opthneg  5086  otthg  5090  opelopabt  5125  opelopabga  5126  brabga  5127  opelopabgf  5133  csbmpt12  5148  rbropapd  5153  dfid3  5163  frirr  5231  wereu2  5251  opeliunxp  5315  posn  5332  sosn  5333  frsn  5334  brab2a  5339  opbrop  5343  csbcnvgALT  5450  elrnmpt1  5517  elrnmptg  5518  opelresg  5545  eliniseg2  5651  poleloe  5673  xpdifid  5708  cnvpo  5822  elpred  5842  ordtri4  5910  oneqmini  5925  elsucg  5941  elsuc2g  5942  sbcfung  6061  dffun8  6065  fncnv  6111  fununi  6113  fnssresb  6152  fnimaeq0  6162  csbfv12  6380  dffn5  6391  funimass4  6397  feqmptdf  6401  fnsnfv  6408  dmfco  6422  fndmdif  6472  fvimacnvi  6482  fvimacnvALT  6487  unpreima  6492  respreima  6495  fmptco  6547  fressnfv  6578  fmptsnd  6587  fnnfpeq0  6596  tpres  6618  elunirn  6660  dff13  6663  f12dfv  6680  f13dfv  6681  fliftel  6710  isoini  6739  f1oiso  6752  riotaeqimp  6785  fnbrovb  6845  eloprabga  6900  resoprab2  6910  elrnmpt2res  6927  ralrnmpt2  6928  ovid  6930  ov  6933  ovg  6952  ofrfval2  7068  dfwe2  7134  ssonprc  7145  ordpwsuc  7168  dfom2  7220  f1oweALT  7305  el2xptp0  7367  fmpt2x  7392  ovmptss  7414  1stconst  7421  2ndconst  7422  fnsuppres  7479  brtpos2  7515  mpt2curryd  7552  dfsmo2  7601  rdglim2  7685  seqomlem2  7703  omeu  7822  oeeui  7839  brdifun  7928  eqerlem  7933  brecop  7995  erovlem  7998  eceqoveq  8007  mapsn  8053  ixpsnval  8065  mptelixpg  8099  map1  8189  xpsnen  8197  xpdom2  8208  omxpenlem  8214  xpf1o  8275  mapunen  8282  onfin  8304  fimaxg  8360  fodomfib  8393  fofinf1o  8394  fipreima  8425  supub  8518  infglb  8549  infglbb  8550  fiming  8557  fiinfg  8558  ordtypecbv  8575  ordtypelem3  8578  ordtypelem9  8584  hartogslem1  8600  wofib  8603  wemapsolem  8608  wemapso2lem  8610  noinfep  8718  cantnf  8751  rankbnd2  8893  domtri2  8976  infxpenc2  9006  fseqdom  9010  acni2  9030  dfac9  9121  cfeq0  9241  cfsuc  9242  cflim3  9247  cfslb  9251  cofsmo  9254  enfin2i  9306  isfin3ds  9314  isf33lem  9351  fin1a2lem5  9389  axdc2lem  9433  zorn2g  9488  fodomb  9511  brdom7disj  9516  brdom6disj  9517  iundom2g  9525  cfpwsdom  9569  elgch  9607  fpwwe2cbv  9615  fpwwecbv  9629  pwfseqlem3  9645  pwfseqlem4a  9646  pwfseqlem4  9647  ltpiord  9872  nlt1pi  9891  nqereu  9914  addclprlem1  10001  1idpr  10014  reclem3pr  10034  ltsosr  10078  map2psrpr  10094  supsrlem  10095  axrrecex  10147  xrlenlt  10266  eqlei2  10311  addsubeq4  10459  renegcli  10505  lesub0  10708  wloglei  10723  conjmul  10905  rereccl  10906  infm3  11145  supaddc  11153  supadd  11154  supmul1  11155  supmullem1  11156  supmullem2  11157  supmul  11158  creui  11178  nndiv  11224  elznn0  11555  prime  11621  eqreznegel  11938  zsupss  11941  rebtwnz  11951  negelrp  12028  ltxr  12113  elixx3g  12352  ixxun  12355  ioo0  12364  ico0  12385  ioc0  12386  icc0  12387  difreicc  12468  divelunit  12478  iccf1o  12480  elfz2  12497  fzn  12521  fznn  12572  fzshftral  12592  nelfzo  12640  fzosplitsni  12744  om2uzisoi  12918  rabssnn0fi  12950  mptnn0fsupp  12962  sq11i  13119  hashsdom  13333  fi1uzind  13442  wrdval  13465  csbwrdg  13491  wrd2ind  13648  s2f1o  13832  cjreb  14033  rexfiuz  14257  cau3lem  14264  rlim2  14397  ello12  14417  ello1mpt  14422  elo12  14428  o1lo1  14438  lo1resb  14465  o1resb  14467  o1compt  14488  caucvgb  14580  pwm1geoser  14770  mertens  14788  ruclem12  15140  divides  15155  dvdsabseq  15208  odd2np1  15238  oddm1even  15240  sumodd  15284  divalgmod  15302  modremain  15305  sadadd2lem2  15345  gcdcllem2  15395  bezoutlem2  15430  bezoutlem3  15431  bezoutlem4  15432  isprm2  15568  isprm3  15569  dvdsnprmd  15576  oddprmdvds  15780  prmreclem2  15794  prmreclem5  15797  prmreclem6  15798  4sqlem2  15826  4sqlem12  15833  vdwmc  15855  vdwpc  15857  vdwlem6  15863  vdwlem10  15867  vdwnn  15875  ramval  15885  0ram  15897  prdsleval  16310  pwsle  16325  imasleval  16374  xpsfrnel2  16398  xpsle  16414  isacs2  16486  mreacs  16491  acsfn  16492  iscatd2  16514  catpropd  16541  ciclcl  16634  cicrcl  16635  isssc  16652  evlfcl  17034  uncfcurf  17051  pltval  17132  lublecllem  17160  tosso  17208  oduleg  17304  oduclatb  17316  posglbmo  17319  isipodrs  17333  odudlatb  17368  gsumvalx  17442  sgrp2rid2  17585  grplmulf1o  17661  grplactcnv  17690  elnmz  17805  eqgid  17818  isghm  17832  ghmeqker  17859  resscntz  17935  symg1bas  17987  pgrpsubgsymgbi  17998  symgfixelq  18024  f1omvdconj  18037  odmulgeq  18145  sylow3lem3  18215  sylow3lem6  18218  efgval2  18308  efgsdm  18314  efgrelexlema  18333  efgcpbllemb  18339  iscyggen2  18454  cyggenod  18457  gsummptfzcl  18539  eldprd  18574  dprdf11  18593  dprddisj2  18609  pgpfac1lem2  18645  pgpfac1  18650  srg1zr  18700  drngid2  18936  issubrg  18953  islmod  19040  aspval2  19520  psrbag  19537  cply1coe0bi  19843  zndvds  20071  znleval  20076  iunocv  20198  pjfval2  20226  pjdm2  20228  dsmmelbas  20256  ellspd  20314  islindf  20324  islindf4  20350  istopg  20873  basgen2  20966  isclo  21064  mretopd  21069  isnei  21080  isperf3  21130  restdis  21155  neitr  21157  restcls  21158  restlp  21160  restperf  21161  iscn  21212  iscnp  21214  lmbr2  21236  lmbrf  21237  ordtt1  21356  cmpsub  21376  hauscmplem  21382  cmpfi  21384  dfconn2  21395  1stcelcls  21437  1stccn  21439  nllyi  21451  subislly  21457  dissnlocfin  21505  elkgen  21512  ptpjpre1  21547  ptuni2  21552  ptclsg  21591  ptcnplem  21597  txcn  21602  hausdiag  21621  txhaus  21623  txkgen  21628  xkoptsub  21630  cnmpt21  21647  elqtop  21673  tgqtop  21688  r0cld  21714  elfg  21847  fbasrn  21860  trfil2  21863  trfil3  21864  fin1aufil  21908  elfm2  21924  elfm3  21926  flimopn  21951  fbflim  21952  flfnei  21967  flftg  21972  cnpflf2  21976  txflf  21982  fclsbas  21997  alexsubALTlem4  22026  cnextfvval  22041  snclseqg  22091  tgphaus  22092  tsmsfbas  22103  tsmssubm  22118  utopsnneip  22224  prdsxmetlem  22345  imasdsf1olem  22350  xpsdsval  22358  blres  22408  isxms2  22425  metcnp  22518  txmetcnp  22524  txmetcn  22525  metustel  22527  metuel2  22542  dscopn  22550  isngp4  22588  cnblcld  22750  metnrmlem1a  22833  icoopnst  22910  iocopnst  22911  elpi1  23016  isclmp  23068  isncvsngp  23120  lmmbr2  23228  cfil3i  23238  caucfil  23252  iscmet3  23262  lmclim  23272  metcld2  23276  bcthlem4  23295  minveclem3b  23370  minveclem6  23376  minveclem7  23377  ivthle  23396  ivthle2  23397  evthicc2  23400  ovolfioo  23407  ovolficc  23408  ovolgelb  23419  dyadmax  23537  subopnmbl  23543  ismbf3d  23591  mbfimaopnlem  23592  mbfimaopn2  23594  mbfaddlem  23597  mbfsup  23601  mbfinf  23602  i1f1lem  23626  i1fmulclem  23639  itg1climres  23651  mbfi1fseqlem4  23655  itg2monolem1  23687  itg2gt0  23697  isibl  23702  iblcnlem1  23724  ellimc2  23811  dvcnvrelem1  23950  itgsubst  23982  mdegleb  23994  fta1glem2  24096  quotval  24217  vieta1lem1  24235  vieta1lem2  24236  ulm2  24309  ulmcaulem  24318  ulmcau  24319  radcnvlt1  24342  sineq0  24443  cos11  24449  recosf1o  24451  efopn  24574  cxpeq  24668  mcubic  24744  birthdaylem3  24850  rlimcnp  24862  xrlimcnp  24865  eldmgm  24918  dmgmaddn0  24919  lgamgulmlem6  24930  wilth  24967  isppw  25010  isppw2  25011  mumullem2  25076  sqff1o  25078  dvdsmulf1o  25090  fsumvma  25108  fsumvma2  25109  vmasum  25111  chpchtsum  25114  lgsne0  25230  gausslemma2dlem0i  25259  gausslemma2dlem1a  25260  lgseisenlem2  25271  lgsquadlem1  25275  lgsquadlem2  25276  2lgslem1a  25286  dchrmusumlema  25352  rpvmasum2  25371  dchrisum0lema  25373  pntibndlem3  25451  pntlemi  25463  pntleml  25470  pnt3  25471  trgcgrg  25580  tgcgr4  25596  colcom  25623  colrot1  25624  ltgov  25662  hlcomb  25668  lncom  25687  mirreu3  25719  isperp  25777  perpcom  25778  brbtwn  25949  brcgr  25950  brbtwn2  25955  colinearalg  25960  axeuclidlem  26012  axcontlem2  26015  axcontlem4  26017  axcontlem7  26020  edgiedgb  26117  isuhgr  26125  isushgr  26126  isupgr  26149  isumgr  26160  isuspgr  26217  isusgr  26218  uhgr0v0e  26300  isfusgrf1  26382  opfusgr  26385  usgr1v0e  26388  dfnbgr3  26401  nbuhgr2vtx1edgb  26418  edgnbusgreu  26438  nbusgredgeu0  26439  isuvtx  26468  isuvtxaOLD  26469  cusgruvtxb  26499  cplgr3v  26512  cusgrsizeinds  26529  vtxdg0v  26550  vtxd0nedgb  26565  vtxduhgr0nedg  26569  vtxdusgr0edgnelALT  26573  iswlk  26687  wlk1walk  26716  upgr2wlk  26745  upgristrl  26780  2pthnloop  26808  usgr2pthlem  26840  isclwlke  26854  isclwlkupgr  26855  iswwlksnx  26914  wwlksnextwrd  26986  wwlksnextproplem3  27000  2pthon3v  27034  umgr2wlk  27040  elwwlks2on  27051  elwwlks2  27059  elwspths2spth  27060  clwwlknclwwlkdif  27071  clwlkclwwlk  27096  clwwlkn1  27141  clwwlkn2  27144  eclclwwlkn1  27177  eleclclwwlkn  27178  hashecclwwlkn1  27179  umgrhashecclwwlk  27180  clwlksfclwwlk1hashnOLD  27184  clwlksfoclwwlkOLD  27188  clwwlknonel  27213  clwwlknon1  27216  clwwlknun  27232  clwwlknunOLD  27236  1pthon2v  27276  uhgr3cyclex  27305  isconngr  27312  isconngr1  27313  eupthres  27338  eupth2lems  27361  isfrgr  27383  frgr0v  27386  frgr3vlem2  27399  fusgr2wsp2nb  27459  extwwlkfab  27482  numclwlk1lem2foa  27484  numclwlk1lem2fo  27488  isvclem  27712  isnvlem  27745  isphg  27952  isph  27957  phoeqi  27993  ubthlem3  28008  minvecolem5  28017  minvecolem6  28018  minvecolem7  28019  hhph  28315  issh3  28356  nmopub  29047  nmfnleub  29064  adjeq  29074  adjvalval  29076  elunop2  29152  lnophm  29158  nmcexi  29165  cnlnadjlem5  29210  cnlnadjeui  29216  adjbd1o  29224  jpi  29409  mddmd2  29448  chrelati  29503  chrelat2i  29504  cvexchlem  29507  dmdbr5ati  29561  cdjreui  29571  cdj3i  29580  iunxsngf  29653  disjunsn  29685  opeldifid  29690  fcoinvbr  29697  brabgaf  29698  opabdm  29701  opabrn  29702  iunsnima  29708  elimampt  29718  abfmpunirn  29732  fmptcof2  29737  funcnvmptOLD  29747  funcnvmpt  29748  funcnv5mpt  29749  f1od2  29779  resf1o  29785  fpwrelmap  29788  iocinioc2  29821  eliccioo  29919  posrasymb  29937  isslmd  30035  smatrcl  30142  pstmxmet  30220  prsdm  30240  prsrn  30241  ordtconnlem1  30250  xrmulc1cn  30256  ispisys2  30496  elcarsg  30647  eulerpartlemmf  30717  isrrvv  30785  reprinrn  30976  tgoldbachgt  31021  bnj976  31126  bnj944  31286  bnj1173  31348  bnj1321  31373  bnj1373  31376  bnj1417  31387  subfacp1lem3  31442  subfacp1lem6  31445  subfacp1  31446  txpconn  31492  sconnpi1  31499  resconn  31506  cvmscbv  31518  cvmsval  31526  cvmlift2lem13  31575  cvmlift3lem2  31580  cvmlift3  31588  mclsrcl  31736  br8  31924  br6  31925  br4  31926  elintfv  31940  fv1stcnv  31956  fv2ndcnv  31957  distel  31985  frpomin  32015  poseq  32030  wsuclem  32047  sltsolem1  32103  nosupdm  32127  nosupbnd1lem4  32134  slenlt  32154  sleloe  32156  etasslt  32197  madeval2  32213  imageval  32314  funpartfv  32329  dfrdg4  32335  altopthg  32351  altopthbg  32352  brcolinear2  32442  lineext  32460  brsegle  32492  seglelin  32500  broutsideof2  32506  isfne4  32612  isfne2  32614  isfne3  32615  fneval  32624  topfneec  32627  neibastop2lem  32632  neibastop2  32633  neifg  32643  filnetlem4  32653  onsuct0  32717  bj-abbi  33052  bj-tagcg  33250  bj-projval  33261  bj-restuni  33327  bj-raldifsn  33331  csbwrecsg  33455  csboprabg  33458  csbmpt22g  33459  topdifinffinlem  33477  isbasisrelowllem1  33485  isbasisrelowllem2  33486  rdgeqoa  33500  csbfinxpg  33507  wl-sbrimt  33613  wl-sblimt  33614  wl-sbnf1  33618  wl-mo2df  33634  wl-eudf  33636  wl-mo2t  33639  wl-mo3t  33640  wl-ax11-lem6  33649  uncov  33672  tan2h  33683  matunitlindf  33689  ptrest  33690  poimirlem2  33693  poimirlem16  33707  poimirlem19  33710  poimirlem23  33714  poimirlem24  33715  poimirlem25  33716  poimirlem26  33717  poimirlem27  33718  mbfposadd  33739  cnambfre  33740  itg2addnclem2  33744  fdc  33823  heibor1  33891  rrncmslem  33913  rrnheibor  33918  opidonOLD  33933  issmgrpOLD  33944  ismndo  33953  isrngo  33978  isdivrngo  34031  isfldidl2  34150  isdmn3  34155  releleccnv  34314  releccnveq  34315  brcnvep  34322  opelresALTV  34324  elecres  34335  eleccnvep  34339  ideq2  34371  extid  34374  relcnveq3  34385  eqres  34401  ecin0  34409  alrmomodm  34416  brxrn  34428  brxrn2  34429  elecxrn  34440  br1cnvxrn2  34446  elec1cnvxrn2  34447  br1cossinres  34489  br1cossxrnres  34490  eldmcoss  34500  elrels2  34528  elrelscnveq3  34533  br1cnvssrres  34547  brcnvssr  34548  dfrefrels2  34555  dfcnvrefrels2  34568  dfsymrels2  34583  elrefsymrelsrel  34609  prtlem13  34626  prter3  34640  lrelat  34773  islshpat  34776  lshpsmreu  34868  lkrpssN  34922  cmtvalN  34970  omllaw2N  35003  cvrval  35028  cvrval2  35033  cvlsupr3  35103  3dim0  35215  islln2  35269  islpln5  35293  islpln2  35294  islpln2ah  35307  islvol5  35337  islvol2  35338  4atlem11  35367  pmapglbx  35527  cdleme18d  36054  cdlemefrs29bpre0  36155  cdlemb3  36365  cdlemg33b  36466  cdlemkid3N  36692  cdlemkid4  36693  dvhb1dimN  36745  dia11N  36808  cdlemm10N  36878  dib11N  36920  dib1dim  36925  dibglbN  36926  diblsmopel  36931  dihopelvalcpre  37008  dih11  37025  dihmeetlem4preN  37066  dihmeetlem13N  37079  lcfrvalsnN  37301  lcfrlem9  37310  lcf1o  37311  mapdval4N  37392  baerlem3lem2  37470  baerlem5alem2  37471  baerlem5blem2  37472  hdmap1fval  37557  hdmapfval  37590  hdmapglem7a  37690  hlhillcs  37721  ellz1  37801  lzunuz  37802  fz1eqin  37803  diophrex  37810  rexrabdioph  37829  rexfrabdioph  37830  2rexfrabdioph  37831  3rexfrabdioph  37832  4rexfrabdioph  37833  6rexfrabdioph  37834  7rexfrabdioph  37835  fzneg  38020  expdioph  38061  wepwsolem  38083  fnwe2lem2  38092  islmodfg  38110  kercvrlsm  38124  sdrgacs  38242  cnvcnvintabd  38377  iunrelexpuztr  38482  brtrclfv2  38490  frege124d  38524  rcompleq  38789  or3or  38790  uneqsn  38792  clsk1independent  38815  ntrclsneine0lem  38833  ntrclsiso  38836  ntrclsk2  38837  ntrclskb  38838  ntrclsk3  38839  ntrclsk13  38840  ntrclsk4  38841  ntrneiel2  38855  ntrneiiso  38860  ntrneikb  38863  ntrneik3  38865  ntrneix3  38866  ntrneik13  38867  ntrneix13  38868  ntrneik4w  38869  k0004lem3  38918  pm10.52  39035  iotasbc  39091  pm14.122a  39094  pm14.122b  39095  pm14.123a  39097  rusbcALT  39111  fvsb  39127  trsbc  39221  sbcel2gOLD  39226  sbcssOLD  39227  csbxpgOLD  39522  csbrngOLD  39525  rexsngf  39688  iunxsngf2  39698  mapsnd  39856  limcperiod  40332  limsupre  40345  dvbdfbdioo  40617  stoweidlem34  40723  fourierdlem108  40903  fourierdlem110  40905  etransc  40972  2reu4a  41664  funressnfv  41683  dfafn5a  41715  elfz2z  41804  el1fzopredsuc  41814  iccelpart  41848  lighneallem2  42002  dfeven2  42041  gbowge7  42130  sbgoldbwt  42144  isupwlk  42196  uspgrsprfo  42235  ismhm0  42284  inclfusubc  42346  isrnghm  42371  rnghmval2  42374  uzlidlring  42408  lidldomnnring  42409  zrninitoringc  42550  opeliun2xp  42590  snlindsntor  42739  elbigo2  42825  gte-lte  42947  gt-lt  42948
  Copyright terms: Public domain W3C validator