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

Theorem syl5bb 284
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 280 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  syl5rbb  285  syl5bbr  286  3bitr4g  315  imim21b  395  ifpfal  1066  norass  1524  cad0  1609  ax12wdemo  2130  eu6lem  2654  abbi  2888  necon3abid  3052  necon3bid  3060  ralxpxfr2d  3638  ceqsrexv  3648  ceqsrex2v  3650  elab2g  3668  elrabf  3675  elrab3t  3678  eueq2  3700  eqreu  3719  reu8  3723  ru  3770  sbcralt  3854  sbcabel  3860  sbcel1g  4364  sbcel2  4366  csbnestgfw  4370  csbnestgf  4375  sbccsb2  4385  2nreu  4391  disjpss  4408  sbcssg  4461  2reu4lem  4463  rexsngOLD  4603  rexsngf  4604  reusngf  4606  ralprgf  4624  rexprgf  4625  reuprg0  4632  difsn  4725  preq2b  4772  opthpr  4776  preqsnd  4783  csbopg  4815  ralunsn  4818  csbuni  4860  dfiin2g  4949  iunxsng  5004  iunxsngf  5006  elpwuni  5019  disjxun  5056  sbcbr12g  5114  opthneg  5365  otthg  5369  opeqsng  5385  snopeqop  5388  opelopabt  5411  opelopabga  5412  brabga  5413  opelopabgf  5419  csbmpt12  5436  rbropapd  5441  dfid3  5456  frirr  5526  wereu2  5546  opeliunxp  5613  posn  5631  sosn  5632  frsn  5633  brab2a  5638  opbrop  5642  csbcnvgALT  5749  dmopabelb  5779  elrnmpt1  5824  elrnmptg  5825  opelres  5853  eliniseg2  5963  poleloe  5985  xpdifid  6019  cnvpo  6132  reu3op  6137  elpred  6155  ordtri4  6222  oneqmini  6236  elsucg  6252  elsuc2g  6253  sbcfung  6373  dffun8  6377  fncnv  6421  fununi  6423  fnssresb  6463  fnimaeq0  6475  csbfv12  6707  dffn5  6718  funimass4  6724  feqmptdf  6729  fnsnfv  6737  dmfco  6751  fndmdif  6805  fvimacnvi  6815  fvimacnvALT  6820  unpreima  6826  respreima  6829  fmptco  6884  fressnfv  6915  fmptsnd  6924  fnnfpeq0  6933  tpres  6956  elunirn  7001  dff13  7004  f12dfv  7021  f13dfv  7022  fliftel  7051  isoini  7080  f1oiso  7093  riotaeqimp  7129  fnbrovb  7194  eloprabga  7250  resoprab2  7260  elrnmpores  7277  ralrnmpo  7278  ovid  7280  ov  7283  ovg  7302  ofrfval2  7416  dfwe2  7484  ssonprc  7495  ordpwsuc  7518  dfom2  7570  f1oweALT  7664  el2xptp0  7727  releldmdifi  7735  fmpox  7756  ovmptss  7779  1stconst  7786  2ndconst  7787  fnsuppres  7848  brtpos2  7889  mpocurryd  7926  dfsmo2  7975  rdglim2  8059  seqomlem2  8078  omeu  8201  oeeui  8218  brdifun  8308  eqerlem  8313  brecop  8380  erovlem  8383  eceqoveq  8392  mapsnd  8439  ixpsnval  8453  mptelixpg  8488  xpsnen  8590  xpdom2  8601  omxpenlem  8607  xpf1o  8668  mapunen  8675  onfin  8698  fimaxg  8754  fodomfib  8787  fofinf1o  8788  fipreima  8819  supub  8912  infglb  8943  infglbb  8944  fiming  8951  fiinfg  8952  ordtypecbv  8970  ordtypelem3  8973  ordtypelem9  8979  hartogslem1  8995  wofib  8998  wemapsolem  9003  wemapso2lem  9005  noinfep  9112  cantnf  9145  rankbnd2  9287  domtri2  9407  infxpenc2  9437  fseqdom  9441  acni2  9461  dfac9  9551  cfeq0  9667  cfsuc  9668  cflim3  9673  cfslb  9677  cofsmo  9680  enfin2i  9732  isfin3ds  9740  isf33lem  9777  fin1a2lem5  9815  axdc2lem  9859  zorn2g  9914  fodomb  9937  brdom7disj  9942  brdom6disj  9943  iundom2g  9951  cfpwsdom  9995  elgch  10033  fpwwe2cbv  10041  fpwwecbv  10055  pwfseqlem3  10071  pwfseqlem4a  10072  pwfseqlem4  10073  ltpiord  10298  nlt1pi  10317  nqereu  10340  addclprlem1  10427  1idpr  10440  reclem3pr  10460  ltsosr  10505  map2psrpr  10521  supsrlem  10522  axrrecex  10574  xrlenlt  10695  eqlei2  10740  addsubeq4  10890  renegcli  10936  lesub0  11146  wloglei  11161  conjmul  11346  rereccl  11347  infm3  11589  supaddc  11597  supadd  11598  supmul1  11599  supmullem1  11600  supmullem2  11601  supmul  11602  creui  11622  nndiv  11672  elznn0  11985  prime  12052  eqreznegel  12323  zsupss  12326  rebtwnz  12336  negelrp  12412  ltxr  12500  elixx3g  12741  ixxun  12744  ioo0  12753  ico0  12774  ioc0  12775  icc0  12776  difreicc  12860  divelunit  12870  iccf1o  12872  elfz2  12889  fzn  12913  fznn  12965  fzshftral  12985  nelfzo  13033  fzosplitsni  13138  om2uzisoi  13312  rabssnn0fi  13344  mptnn0fsupp  13355  sq11i  13544  hashsdom  13732  fi1uzind  13845  wrdval  13854  csbwrdg  13885  wrd2ind  14075  s2f1o  14268  cjreb  14472  rexfiuz  14697  cau3lem  14704  rlim2  14843  ello12  14863  ello1mpt  14868  elo12  14874  o1lo1  14884  lo1resb  14911  o1resb  14913  o1compt  14934  caucvgb  15026  pwm1geoserOLD  15215  mertens  15232  ruclem12  15584  divides  15599  dvdsabseq  15653  odd2np1  15680  oddm1even  15682  sumodd  15729  divalgmod  15747  modremain  15749  sadadd2lem2  15789  gcdcllem2  15839  bezoutlem2  15878  bezoutlem3  15879  bezoutlem4  15880  isprm2  16016  isprm3  16017  dvdsnprmd  16024  oddprmdvds  16229  prmreclem2  16243  prmreclem5  16246  prmreclem6  16247  4sqlem2  16275  4sqlem12  16282  vdwmc  16304  vdwpc  16306  vdwlem6  16312  vdwlem10  16316  vdwnn  16324  ramval  16334  0ram  16346  prdsleval  16740  pwsle  16755  imasleval  16804  xpsfrnel2  16827  xpsle  16842  isacs2  16914  mreacs  16919  acsfn  16920  iscatd2  16942  catpropd  16969  ciclcl  17062  cicrcl  17063  isssc  17080  evlfcl  17462  uncfcurf  17479  pltval  17560  lublecllem  17588  tosso  17636  oduleg  17732  oduclatb  17744  posglbmo  17747  isipodrs  17761  odudlatb  17796  gsumvalx  17876  sgrp2rid2  18031  grplmulf1o  18113  grplactcnv  18142  elnmz  18255  eqgid  18272  isghm  18298  ghmeqker  18325  resscntz  18402  symg1bas  18455  pgrpsubgsymgbi  18467  symgfixelq  18492  f1omvdconj  18505  odmulgeq  18615  sylow3lem3  18685  sylow3lem6  18688  efgval2  18781  efgsdm  18787  efgrelexlema  18806  efgcpbllemb  18812  iscyggen2  18931  cyggenod  18934  gsummptfzcl  19020  eldprd  19057  dprdf11  19076  dprddisj2  19092  pgpfac1lem2  19128  pgpfac1  19133  srg1zr  19210  drngid2  19449  issubrg  19466  sdrgacs  19511  islmod  19569  aspval2  20057  psrbag  20074  cply1coe0bi  20398  zndvds  20626  znleval  20631  iunocv  20755  pjfval2  20783  pjdm2  20785  dsmmelbas  20813  ellspd  20876  islindf  20886  islindf4  20912  istopg  21433  basgen2  21527  isclo  21625  mretopd  21630  isnei  21641  isperf3  21691  restdis  21716  neitr  21718  restcls  21719  restlp  21721  restperf  21722  iscn  21773  iscnp  21775  lmbr2  21797  lmbrf  21798  ordtt1  21917  cmpsub  21938  hauscmplem  21944  cmpfi  21946  dfconn2  21957  1stcelcls  21999  1stccn  22001  nllyi  22013  subislly  22019  dissnlocfin  22067  elkgen  22074  ptpjpre1  22109  ptuni2  22114  ptclsg  22153  ptcnplem  22159  txcn  22164  hausdiag  22183  txhaus  22185  txkgen  22190  xkoptsub  22192  cnmpt21  22209  elqtop  22235  tgqtop  22250  r0cld  22276  elfg  22409  fbasrn  22422  trfil2  22425  trfil3  22426  fin1aufil  22470  elfm2  22486  elfm3  22488  flimopn  22513  fbflim  22514  flfnei  22529  flftg  22534  cnpflf2  22538  txflf  22544  fclsbas  22559  alexsubALTlem4  22588  cnextfvval  22603  snclseqg  22653  tgphaus  22654  tsmsfbas  22665  tsmssubm  22680  utopsnneip  22786  prdsxmetlem  22907  imasdsf1olem  22912  xpsdsval  22920  blres  22970  isxms2  22987  metcnp  23080  txmetcnp  23086  txmetcn  23087  metustel  23089  metuel2  23104  dscopn  23112  isngp4  23150  cnblcld  23312  metnrmlem1a  23395  icoopnst  23472  iocopnst  23473  elpi1  23578  isclmp  23630  isncvsngp  23682  lmmbr2  23791  cfil3i  23801  caucfil  23815  iscmet3  23825  lmclim  23835  metcld2  23839  bcthlem4  23859  minveclem3b  23960  minveclem6  23966  minveclem7  23967  ivthle  23986  ivthle2  23987  evthicc2  23990  ovolfioo  23997  ovolficc  23998  ovolgelb  24010  dyadmax  24128  subopnmbl  24134  ismbf3d  24184  mbfimaopnlem  24185  mbfimaopn2  24187  mbfaddlem  24190  mbfsup  24194  mbfinf  24195  i1f1lem  24219  i1fmulclem  24232  itg1climres  24244  mbfi1fseqlem4  24248  itg2monolem1  24280  itg2gt0  24290  isibl  24295  iblcnlem1  24317  ellimc2  24404  dvcnvrelem1  24543  itgsubst  24575  mdegleb  24587  fta1glem2  24689  quotval  24810  vieta1lem1  24828  vieta1lem2  24829  ulm2  24902  ulmcaulem  24911  ulmcau  24912  radcnvlt1  24935  sineq0  25038  cos11  25044  recosf1o  25046  efopn  25168  cxpeq  25265  mcubic  25352  birthdaylem3  25459  rlimcnp  25471  xrlimcnp  25474  eldmgm  25527  dmgmaddn0  25528  lgamgulmlem6  25539  wilth  25576  isppw  25619  isppw2  25620  mumullem2  25685  sqff1o  25687  dvdsmulf1o  25699  fsumvma  25717  fsumvma2  25718  vmasum  25720  chpchtsum  25723  lgsne0  25839  gausslemma2dlem0i  25868  gausslemma2dlem1a  25869  lgseisenlem2  25880  lgsquadlem1  25884  lgsquadlem2  25885  2lgslem1a  25895  addsq2reu  25944  2sqreu  25960  2sqreunn  25961  2sqreult  25962  2sqreunnlt  25964  dchrmusumlema  25997  rpvmasum2  26016  dchrisum0lema  26018  pntibndlem3  26096  pntlemi  26108  pntleml  26115  pnt3  26116  trgcgrg  26229  tgcgr4  26245  colcom  26272  colrot1  26273  ltgov  26311  hlcomb  26317  lncom  26336  mirreu3  26368  isperp  26426  perpcom  26427  iscgra  26523  isinag  26552  brbtwn  26613  brcgr  26614  brbtwn2  26619  colinearalg  26624  axeuclidlem  26676  axcontlem2  26679  axcontlem4  26681  axcontlem7  26684  elntg2  26699  edgiedgb  26767  isuhgr  26773  isushgr  26774  isupgr  26797  isumgr  26808  isuspgr  26865  isusgr  26866  uhgr0v0e  26948  isfusgrf1  27030  opfusgr  27033  usgr1v0e  27036  dfnbgr3  27048  nbuhgr2vtx1edgb  27062  edgnbusgreu  27077  nbusgredgeu0  27078  isuvtx  27105  cusgruvtxb  27132  cplgr3v  27145  cusgrsizeinds  27162  vtxdg0v  27183  vtxd0nedgb  27198  vtxduhgr0nedg  27202  vtxdusgr0edgnelALT  27206  iswlk  27320  wlk1walk  27348  upgr2wlk  27378  upgristrl  27412  2pthnloop  27440  usgr2pthlem  27472  isclwlke  27486  isclwlkupgr  27487  iswwlksnx  27546  wwlksnextwrd  27603  wwlksnextproplem3  27618  2pthon3v  27650  umgr2wlk  27656  elwwlks2on  27666  elwwlks2  27673  elwspths2spth  27674  clwwlknclwwlkdif  27685  clwlkclwwlk  27708  clwlkclwwlk2  27709  clwwlkn1  27747  clwwlkn2  27750  clwwlkwwlksb  27761  eclclwwlkn1  27782  eleclclwwlkn  27783  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknonel  27802  clwwlknon1  27804  clwwlknun  27819  1pthon2v  27860  uhgr3cyclex  27889  isconngr  27896  isconngr1  27897  eupthres  27922  eupth2lems  27945  frgr0v  27969  frgr3vlem2  27981  fusgr2wsp2nb  28041  extwwlkfab  28059  numclwwlk1lem2foa  28061  numclwwlk1lem2fo  28065  isvclem  28282  isnvlem  28315  isphg  28522  isph  28527  phoeqi  28562  ubthlem3  28577  minvecolem5  28586  minvecolem6  28587  minvecolem7  28588  hhph  28883  issh3  28924  nmopub  29613  nmfnleub  29630  adjeq  29640  adjvalval  29642  elunop2  29718  lnophm  29724  nmcexi  29731  cnlnadjlem5  29776  cnlnadjeui  29782  adjbd1o  29790  jpi  29975  mddmd2  30014  chrelati  30069  chrelat2i  30070  cvexchlem  30073  dmdbr5ati  30127  cdjreui  30137  cdj3i  30146  elunsn  30201  disjunsn  30273  opeldifid  30278  fcoinvbr  30287  brabgaf  30288  opabdm  30291  opabrn  30292  iunsnima  30298  nfpconfp  30306  elimampt  30312  abfmpunirn  30326  fmptcof2  30331  funcnvmpt  30341  funcnv5mpt  30342  brsnop  30356  brprop  30360  f1od2  30384  resf1o  30393  fpwrelmap  30396  iocinioc2  30429  eliccioo  30535  wrdt2ind  30555  posrasymb  30572  isslmd  30758  fedgmullem2  30926  smatrcl  30961  pstmxmet  31037  prsdm  31057  prsrn  31058  ordtconnlem1  31067  xrmulc1cn  31073  ispisys2  31312  elcarsg  31463  eulerpartlemmf  31533  isrrvv  31601  reprinrn  31789  tgoldbachgt  31834  bnj976  31949  bnj944  32110  bnj1173  32172  bnj1321  32197  bnj1373  32200  bnj1417  32211  lfuhgr  32262  revwlk  32269  usgrgt2cycl  32275  subfacp1lem3  32327  subfacp1lem6  32330  subfacp1  32331  txpconn  32377  sconnpi1  32384  resconn  32391  cvmscbv  32403  cvmsval  32411  cvmlift2lem13  32460  cvmlift3lem2  32465  cvmlift3  32473  goeleq12bg  32494  satfvsucsuc  32510  satfbrsuc  32511  fmlafvel  32530  satffunlem2lem1  32549  satefvfmla1  32570  mclsrcl  32706  br8  32890  br6  32891  br4  32892  elintfv  32905  fv1stcnv  32918  fv2ndcnv  32919  distel  32946  frpomin  32976  poseq  32993  wsuclem  33010  sltsolem1  33078  nosupdm  33102  nosupbnd1lem4  33109  slenlt  33129  sleloe  33131  etasslt  33172  madeval2  33188  imageval  33289  funpartfv  33304  dfrdg4  33310  altopthg  33326  altopthbg  33327  brcolinear2  33417  lineext  33435  brsegle  33467  seglelin  33475  broutsideof2  33481  isfne4  33586  isfne2  33588  isfne3  33589  fneval  33598  topfneec  33601  neibastop2lem  33606  neibastop2  33607  neifg  33617  filnetlem4  33627  onsuct0  33687  bj-19.41t  34001  bj-tagcg  34195  bj-projval  34206  bj-restuni  34283  opelopabd  34326  opelopabb  34327  brabd0  34332  bj-opelid  34341  bj-ideqg  34342  bj-opelidres  34346  bj-ideqg1  34349  bj-elid6  34355  bj-isvec  34458  bj-isclm  34461  bj-isrvecd  34468  csbwrecsg  34491  csboprabg  34494  csbmpo123  34495  topdifinffinlem  34511  isbasisrelowllem1  34519  isbasisrelowllem2  34520  rdgeqoa  34534  csbfinxpg  34552  nlpineqsn  34572  wl-sbrimt  34668  wl-sblimt  34669  wl-sbnf1  34673  wl-mo2df  34688  wl-eudf  34690  wl-mo2t  34693  wl-mo3t  34694  wl-ax11-lem6  34704  wl-dfclab  34710  uncov  34755  tan2h  34766  matunitlindf  34772  ptrest  34773  poimirlem2  34776  poimirlem16  34790  poimirlem19  34793  poimirlem23  34797  poimirlem24  34798  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  mbfposadd  34821  cnambfre  34822  itg2addnclem2  34826  fdc  34903  heibor1  34971  rrncmslem  34993  rrnheibor  34998  opidonOLD  35013  issmgrpOLD  35024  ismndo  35033  isrngo  35058  isdivrngo  35111  isfldidl2  35230  isdmn3  35235  releleccnv  35401  releccnveq  35402  brcnvep  35409  elecres  35417  eleccnvep  35421  ideq2  35448  extid  35451  relcnveq3  35461  eqres  35480  brrabga  35481  ecin0  35489  alrmomodm  35496  brxrn  35508  brxrn2  35509  elecxrn  35520  br1cnvxrn2  35526  elec1cnvxrn2  35527  br1cossinres  35569  br1cossxrnres  35570  eldmcoss  35580  elrels2  35608  elrelscnveq3  35613  br1cnvssrres  35627  brcnvssr  35628  dfrefrels2  35635  dfcnvrefrels2  35648  dfsymrels2  35663  elrefsymrelsrel  35689  dftrrels2  35693  erim2  35793  eldisjs5  35841  prtlem13  35886  prter3  35900  lrelat  36032  islshpat  36035  lshpsmreu  36127  lkrpssN  36181  cmtvalN  36229  omllaw2N  36262  cvrval  36287  cvrval2  36292  cvlsupr3  36362  3dim0  36475  islln2  36529  islpln5  36553  islpln2  36554  islpln2ah  36567  islvol5  36597  islvol2  36598  4atlem11  36627  pmapglbx  36787  cdleme18d  37313  cdlemefrs29bpre0  37414  cdlemb3  37624  cdlemg33b  37725  cdlemkid3N  37951  cdlemkid4  37952  dvhb1dimN  38004  dia11N  38066  cdlemm10N  38136  dib11N  38178  dib1dim  38183  dibglbN  38184  diblsmopel  38189  dihopelvalcpre  38266  dih11  38283  dihmeetlem4preN  38324  dihmeetlem13N  38337  lcfrvalsnN  38559  lcfrlem9  38568  lcf1o  38569  mapdval4N  38650  baerlem3lem2  38728  baerlem5alem2  38729  baerlem5blem2  38730  hdmap1fval  38814  hdmapfval  38845  hdmapglem7a  38945  hlhillcs  38976  frlmfielbas  39019  addsubeq4com  39046  prjspreln0  39139  ellz1  39244  lzunuz  39245  fz1eqin  39246  diophrex  39252  rexrabdioph  39271  rexfrabdioph  39272  2rexfrabdioph  39273  3rexfrabdioph  39274  4rexfrabdioph  39275  6rexfrabdioph  39276  7rexfrabdioph  39277  fzneg  39459  expdioph  39500  wepwsolem  39522  fnwe2lem2  39531  islmodfg  39549  kercvrlsm  39563  cnvcnvintabd  39840  iunrelexpuztr  39944  brtrclfv2  39952  frege124d  39986  rcompleq  40250  or3or  40251  uneqsn  40253  clsk1independent  40276  ntrclsneine0lem  40294  ntrclsiso  40297  ntrclsk2  40298  ntrclskb  40299  ntrclsk3  40300  ntrclsk13  40301  ntrclsk4  40302  ntrneiel2  40316  ntrneiiso  40321  ntrneikb  40324  ntrneik3  40326  ntrneix3  40327  ntrneik13  40328  ntrneix13  40329  ntrneik4w  40330  k0004lem3  40379  scottabf  40456  pm10.52  40577  iotasbc  40631  pm14.122a  40634  pm14.122b  40635  pm14.123a  40637  rusbcALT  40651  fvsb  40664  trsbc  40754  wessf1ornlem  41325  imassmpt  41417  limcperiod  41789  limsupre  41802  dvbdfbdioo  42095  stoweidlem34  42200  fourierdlem108  42380  fourierdlem110  42382  etransc  42449  funressnfv  43159  dfafn5a  43240  ndfatafv2nrn  43301  afv2ndefb  43304  dfatsnafv2  43332  dfatdmfcoafv2  43334  dfatco  43336  afv2fv0xorb  43347  readdcnnred  43384  resubcnnred  43385  recnmulnred  43386  cndivrenred  43387  elfz2z  43396  el1fzopredsuc  43406  iccelpart  43440  ichal  43474  reupr  43531  lighneallem2  43618  dfeven2  43661  gbowge7  43775  sbgoldbwt  43789  isupwlk  43858  uspgrsprfo  43870  ismhm0  43919  elefmndbas  43941  elefmndbas2  43942  inclfusubc  44036  isrnghm  44061  rnghmval2  44064  uzlidlring  44098  lidldomnnring  44099  zrninitoringc  44240  opeliun2xp  44279  snlindsntor  44424  elbigo2  44510  resum2sqorgt0  44594  rrx2pnedifcoorneor  44601  rrx2plord  44605  rrx2plordisom  44608  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  rrx2linest2  44629  itsclc0b  44657  itsclinecirc0in  44660  inlinecirc02plem  44671  gte-lte  44721  gt-lt  44722
  Copyright terms: Public domain W3C validator