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

Theorem syl5bb 286
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 282 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  syl5rbb  287  syl5bbr  288  3bitr4g  317  imim21b  398  ifpfal  1072  norass  1534  cad0  1619  ax12wdemo  2140  eu6lem  2658  abbi  2888  necon3abid  3043  necon3bid  3051  ralxpxfr2d  3616  ceqsrexv  3626  ceqsrex2v  3628  elab2gw  3642  elab2g  3645  elrabf  3653  elrab3t  3656  eueq2  3678  eqreu  3697  reu8  3701  ru  3748  sbcralt  3830  sbcabel  3836  sbcel1g  4338  sbcel2  4340  csbnestgfw  4344  csbnestgf  4349  sbccsb2  4359  2nreu  4366  disjpss  4383  sbcssg  4436  2reu4lem  4438  rexsngf  4583  reusngf  4585  ralprgf  4603  rexprgf  4604  reuprg0  4611  difsn  4704  preq2b  4751  opthpr  4755  preqsnd  4762  csbopg  4794  ralunsn  4797  csbuni  4840  dfiin2g  4930  iunxsng  4985  iunxsngf  4987  elpwuni  5000  disjxun  5037  sbcbr12g  5095  opthneg  5346  otthg  5350  opeqsng  5366  snopeqop  5369  opelopabt  5392  opelopabga  5393  brabga  5394  opelopabgf  5400  csbmpt12  5417  rbropapd  5422  dfid3  5435  frirr  5505  wereu2  5525  opeliunxp  5592  posn  5610  sosn  5611  frsn  5612  brab2a  5617  opbrop  5621  csbcnvgALT  5728  dmopabelb  5758  elrnmpt1  5803  elrnmptg  5804  opelres  5832  eliniseg2  5942  poleloe  5964  xpdifid  5998  cnvpo  6111  reu3op  6116  elpred  6134  ordtri4  6201  oneqmini  6215  elsucg  6231  elsuc2g  6232  sbcfung  6352  dffun8  6356  fncnv  6400  fununi  6402  fnssresb  6442  fnimaeq0  6454  csbfv12  6686  dffn5  6697  funimass4  6703  feqmptdf  6708  fnsnfv  6716  dmfco  6730  fndmdif  6785  fvimacnvi  6795  fvimacnvALT  6800  unpreima  6806  respreima  6809  fmptco  6864  fressnfv  6895  fmptsnd  6904  fnnfpeq0  6913  tpres  6936  elunirn  6984  dff13  6987  f12dfv  7004  f13dfv  7005  fliftel  7036  isoini  7065  f1oiso  7078  riotaeqimp  7114  fnbrovb  7179  eloprabga  7235  resoprab2  7245  elrnmpores  7262  ralrnmpo  7263  ovid  7265  ov  7268  ovg  7288  ofrfval2  7402  dfwe2  7471  ssonprc  7482  ordpwsuc  7505  dfom2  7557  f1oweALT  7648  el2xptp0  7711  releldmdifi  7719  fmpox  7740  ovmptss  7763  1stconst  7770  2ndconst  7771  fnsuppres  7832  brtpos2  7873  mpocurryd  7910  dfsmo2  7959  rdglim2  8043  seqomlem2  8062  omeu  8186  oeeui  8203  brdifun  8293  eqerlem  8298  brecop  8365  erovlem  8368  eceqoveq  8377  mapsnd  8425  ixpsnval  8439  mptelixpg  8474  xpsnen  8576  xpdom2  8587  omxpenlem  8593  xpf1o  8655  mapunen  8662  onfin  8686  fimaxg  8741  fodomfib  8774  fofinf1o  8775  fipreima  8806  supub  8899  infglb  8930  infglbb  8931  fiming  8938  fiinfg  8939  ordtypecbv  8957  ordtypelem3  8960  ordtypelem9  8966  hartogslem1  8982  wofib  8985  wemapsolem  8990  wemapso2lem  8992  noinfep  9099  cantnf  9132  rankbnd2  9274  domtri2  9394  infxpenc2  9425  fseqdom  9429  acni2  9449  dfac9  9539  cfeq0  9655  cfsuc  9656  cflim3  9661  cfslb  9665  cofsmo  9668  enfin2i  9720  isfin3ds  9728  isf33lem  9765  fin1a2lem5  9803  axdc2lem  9847  zorn2g  9902  fodomb  9925  brdom7disj  9930  brdom6disj  9931  iundom2g  9939  cfpwsdom  9983  elgch  10021  fpwwe2cbv  10029  fpwwecbv  10043  pwfseqlem3  10059  pwfseqlem4a  10060  pwfseqlem4  10061  ltpiord  10286  nlt1pi  10305  nqereu  10328  addclprlem1  10415  1idpr  10428  reclem3pr  10448  ltsosr  10493  map2psrpr  10509  supsrlem  10510  axrrecex  10562  xrlenlt  10683  eqlei2  10728  addsubeq4  10878  renegcli  10924  lesub0  11134  wloglei  11149  conjmul  11334  rereccl  11335  infm3  11577  supaddc  11585  supadd  11586  supmul1  11587  supmullem1  11588  supmullem2  11589  supmul  11590  creui  11610  nndiv  11661  elznn0  11974  prime  12041  eqreznegel  12312  zsupss  12315  rebtwnz  12325  negelrp  12400  ltxr  12488  elixx3g  12729  ixxun  12732  ioo0  12741  ico0  12762  ioc0  12763  icc0  12764  difreicc  12852  divelunit  12862  iccf1o  12864  elfz2  12882  fzn  12906  fznn  12958  fzshftral  12978  nelfzo  13026  fzosplitsni  13131  om2uzisoi  13305  rabssnn0fi  13337  mptnn0fsupp  13348  sq11i  13538  hashsdom  13726  fi1uzind  13839  wrdval  13848  csbwrdg  13875  wrd2ind  14064  s2f1o  14257  cjreb  14461  rexfiuz  14686  cau3lem  14693  rlim2  14832  ello12  14852  ello1mpt  14857  elo12  14863  o1lo1  14873  lo1resb  14900  o1resb  14902  o1compt  14923  caucvgb  15015  pwm1geoserOLD  15204  mertens  15221  ruclem12  15573  divides  15588  dvdsabseq  15642  odd2np1  15669  oddm1even  15671  sumodd  15716  divalgmod  15734  modremain  15736  sadadd2lem2  15776  gcdcllem2  15826  bezoutlem2  15865  bezoutlem3  15866  bezoutlem4  15867  isprm2  16003  isprm3  16004  dvdsnprmd  16011  oddprmdvds  16216  prmreclem2  16230  prmreclem5  16233  prmreclem6  16234  4sqlem2  16262  4sqlem12  16269  vdwmc  16291  vdwpc  16293  vdwlem6  16299  vdwlem10  16303  vdwnn  16311  ramval  16321  0ram  16333  prdsleval  16729  pwsle  16744  imasleval  16793  xpsfrnel2  16816  xpsle  16831  isacs2  16903  mreacs  16908  acsfn  16909  iscatd2  16931  catpropd  16958  ciclcl  17051  cicrcl  17052  isssc  17069  evlfcl  17451  uncfcurf  17468  pltval  17549  lublecllem  17577  tosso  17625  oduleg  17721  oduclatb  17733  posglbmo  17736  isipodrs  17750  odudlatb  17785  gsumvalx  17865  elefmndbas  18017  sgrp2rid2  18070  grplmulf1o  18152  grplactcnv  18181  elnmz  18294  eqgid  18311  isghm  18337  ghmeqker  18364  resscntz  18441  symg1bas  18498  pgrpsubgsymgbi  18515  symgfixelq  18540  f1omvdconj  18553  odmulgeq  18663  sylow3lem3  18733  sylow3lem6  18736  efgval2  18829  efgsdm  18835  efgrelexlema  18854  efgcpbllemb  18860  iscyggen2  18979  cyggenod  18982  gsummptfzcl  19068  eldprd  19105  dprdf11  19124  dprddisj2  19140  pgpfac1lem2  19176  pgpfac1  19181  srg1zr  19258  drngid2  19494  issubrg  19511  sdrgacs  19556  islmod  19614  aspval2  20103  psrbag  20120  cply1coe0bi  20444  zndvds  20672  znleval  20677  iunocv  20801  pjfval2  20829  pjdm2  20831  dsmmelbas  20859  ellspd  20922  islindf  20932  islindf4  20958  istopg  21479  basgen2  21573  isclo  21671  mretopd  21676  isnei  21687  isperf3  21737  restdis  21762  neitr  21764  restcls  21765  restlp  21767  restperf  21768  iscn  21819  iscnp  21821  lmbr2  21843  lmbrf  21844  ordtt1  21963  cmpsub  21984  hauscmplem  21990  cmpfi  21992  dfconn2  22003  1stcelcls  22045  1stccn  22047  nllyi  22059  subislly  22065  dissnlocfin  22113  elkgen  22120  ptpjpre1  22155  ptuni2  22160  ptclsg  22199  ptcnplem  22205  txcn  22210  hausdiag  22229  txhaus  22231  txkgen  22236  xkoptsub  22238  cnmpt21  22255  elqtop  22281  tgqtop  22296  r0cld  22322  elfg  22455  fbasrn  22468  trfil2  22471  trfil3  22472  fin1aufil  22516  elfm2  22532  elfm3  22534  flimopn  22559  fbflim  22560  flfnei  22575  flftg  22580  cnpflf2  22584  txflf  22590  fclsbas  22605  alexsubALTlem4  22634  cnextfvval  22649  snclseqg  22700  tgphaus  22701  tsmsfbas  22712  tsmssubm  22727  utopsnneip  22833  prdsxmetlem  22954  imasdsf1olem  22959  xpsdsval  22967  blres  23017  isxms2  23034  metcnp  23127  txmetcnp  23133  txmetcn  23134  metustel  23136  metuel2  23151  dscopn  23159  isngp4  23197  cnblcld  23359  metnrmlem1a  23442  icoopnst  23523  iocopnst  23524  elpi1  23629  isclmp  23681  isncvsngp  23733  lmmbr2  23842  cfil3i  23852  caucfil  23866  iscmet3  23876  lmclim  23886  metcld2  23890  bcthlem4  23910  minveclem3b  24011  minveclem6  24017  minveclem7  24018  ivthle  24039  ivthle2  24040  evthicc2  24043  ovolfioo  24050  ovolficc  24051  ovolgelb  24063  dyadmax  24181  subopnmbl  24187  ismbf3d  24237  mbfimaopnlem  24238  mbfimaopn2  24240  mbfaddlem  24243  mbfsup  24247  mbfinf  24248  i1f1lem  24272  i1fmulclem  24285  itg1climres  24297  mbfi1fseqlem4  24301  itg2monolem1  24333  itg2gt0  24343  isibl  24348  iblcnlem1  24370  ellimc2  24459  dvcnvrelem1  24599  itgsubst  24631  mdegleb  24644  fta1glem2  24746  quotval  24867  vieta1lem1  24885  vieta1lem2  24886  ulm2  24959  ulmcaulem  24968  ulmcau  24969  radcnvlt1  24992  sineq0  25095  cos11  25104  recosf1o  25106  efopn  25228  cxpeq  25325  mcubic  25412  birthdaylem3  25518  rlimcnp  25530  xrlimcnp  25533  eldmgm  25586  dmgmaddn0  25587  lgamgulmlem6  25598  wilth  25635  isppw  25678  isppw2  25679  mumullem2  25744  sqff1o  25746  dvdsmulf1o  25758  fsumvma  25776  fsumvma2  25777  vmasum  25779  chpchtsum  25782  lgsne0  25898  gausslemma2dlem0i  25927  gausslemma2dlem1a  25928  lgseisenlem2  25939  lgsquadlem1  25943  lgsquadlem2  25944  2lgslem1a  25954  addsq2reu  26003  2sqreu  26019  2sqreunn  26020  2sqreult  26021  2sqreunnlt  26023  dchrmusumlema  26056  rpvmasum2  26075  dchrisum0lema  26077  pntibndlem3  26155  pntlemi  26167  pntleml  26174  pnt3  26175  trgcgrg  26288  tgcgr4  26304  colcom  26331  colrot1  26332  ltgov  26370  hlcomb  26376  lncom  26395  mirreu3  26427  isperp  26485  perpcom  26486  iscgra  26582  isinag  26611  brbtwn  26672  brcgr  26673  brbtwn2  26678  colinearalg  26683  axeuclidlem  26735  axcontlem2  26738  axcontlem4  26740  axcontlem7  26743  elntg2  26758  edgiedgb  26826  isuhgr  26832  isushgr  26833  isupgr  26856  isumgr  26867  isuspgr  26924  isusgr  26925  uhgr0v0e  27007  isfusgrf1  27089  opfusgr  27092  usgr1v0e  27095  dfnbgr3  27107  nbuhgr2vtx1edgb  27121  edgnbusgreu  27136  nbusgredgeu0  27137  isuvtx  27164  cusgruvtxb  27191  cplgr3v  27204  cusgrsizeinds  27221  vtxdg0v  27242  vtxd0nedgb  27257  vtxduhgr0nedg  27261  vtxdusgr0edgnelALT  27265  iswlk  27379  wlk1walk  27407  upgr2wlk  27437  upgristrl  27471  2pthnloop  27499  usgr2pthlem  27531  isclwlke  27545  isclwlkupgr  27546  iswwlksnx  27605  wwlksnextwrd  27662  wwlksnextproplem3  27676  2pthon3v  27708  umgr2wlk  27714  elwwlks2on  27724  elwwlks2  27731  elwspths2spth  27732  clwwlknclwwlkdif  27743  clwlkclwwlk  27766  clwlkclwwlk2  27767  clwwlkn1  27805  clwwlkn2  27808  clwwlkwwlksb  27818  eclclwwlkn1  27839  eleclclwwlkn  27840  hashecclwwlkn1  27841  umgrhashecclwwlk  27842  clwwlknonel  27859  clwwlknon1  27861  clwwlknun  27876  1pthon2v  27917  uhgr3cyclex  27946  isconngr  27953  isconngr1  27954  eupthres  27979  eupth2lems  28002  frgr0v  28026  frgr3vlem2  28038  fusgr2wsp2nb  28098  extwwlkfab  28116  numclwwlk1lem2foa  28118  numclwwlk1lem2fo  28122  isvclem  28339  isnvlem  28372  isphg  28579  isph  28584  phoeqi  28619  ubthlem3  28634  minvecolem5  28643  minvecolem6  28644  minvecolem7  28645  hhph  28940  issh3  28981  nmopub  29670  nmfnleub  29687  adjeq  29697  adjvalval  29699  elunop2  29775  lnophm  29781  nmcexi  29788  cnlnadjlem5  29833  cnlnadjeui  29839  adjbd1o  29847  jpi  30032  mddmd2  30071  chrelati  30126  chrelat2i  30127  cvexchlem  30130  dmdbr5ati  30184  cdjreui  30194  cdj3i  30203  elunsn  30259  disjunsn  30331  opeldifid  30336  fcoinvbr  30345  brabgaf  30346  opabdm  30349  opabrn  30350  iunsnima  30356  nfpconfp  30364  elimampt  30370  abfmpunirn  30384  fmptcof2  30389  funcnvmpt  30399  funcnv5mpt  30400  brsnop  30416  brprop  30420  f1od2  30444  resf1o  30453  fpwrelmap  30456  iocinioc2  30489  eliccioo  30594  wrdt2ind  30614  posrasymb  30631  mcgcnv  30666  isslmd  30838  fedgmullem2  31037  smatrcl  31072  pstmxmet  31148  prsdm  31165  prsrn  31166  ordtconnlem1  31175  xrmulc1cn  31181  ispisys2  31420  elcarsg  31571  eulerpartlemmf  31641  isrrvv  31709  reprinrn  31897  tgoldbachgt  31942  bnj976  32057  bnj944  32218  bnj1173  32282  bnj1321  32307  bnj1373  32310  bnj1417  32321  lfuhgr  32372  revwlk  32379  usgrgt2cycl  32385  subfacp1lem3  32437  subfacp1lem6  32440  subfacp1  32441  txpconn  32487  sconnpi1  32494  resconn  32501  cvmscbv  32513  cvmsval  32521  cvmlift2lem13  32570  cvmlift3lem2  32575  cvmlift3  32583  goeleq12bg  32604  satfvsucsuc  32620  satfbrsuc  32621  fmlafvel  32640  satffunlem2lem1  32659  satefvfmla1  32680  mclsrcl  32816  br8  33000  br6  33001  br4  33002  elintfv  33015  fv1stcnv  33028  fv2ndcnv  33029  distel  33056  frpomin  33086  poseq  33103  wsuclem  33120  sltsolem1  33188  nosupdm  33212  nosupbnd1lem4  33219  slenlt  33239  sleloe  33241  etasslt  33282  madeval2  33298  imageval  33399  funpartfv  33414  dfrdg4  33420  altopthg  33436  altopthbg  33437  brcolinear2  33527  lineext  33545  brsegle  33577  seglelin  33585  broutsideof2  33591  isfne4  33696  isfne2  33698  isfne3  33699  fneval  33708  topfneec  33711  neibastop2lem  33716  neibastop2  33717  neifg  33727  filnetlem4  33737  onsuct0  33797  bj-19.41t  34112  bj-tagcg  34315  bj-projval  34326  bj-restuni  34406  opelopabd  34451  opelopabb  34452  brabd0  34457  bj-opelid  34466  bj-ideqg  34467  bj-opelidres  34471  bj-ideqg1  34474  bj-elid6  34480  bj-isvec  34591  bj-isclm  34594  bj-isrvecd  34601  csbwrecsg  34632  csboprabg  34635  csbmpo123  34636  topdifinffinlem  34652  isbasisrelowllem1  34660  isbasisrelowllem2  34661  rdgeqoa  34675  csbfinxpg  34693  nlpineqsn  34713  wl-3xortru  34772  wl-3xorfal  34773  wl-3mintru2tru  34790  wl-3mintru2fal  34791  wl-sbrimt  34837  wl-sblimt  34838  wl-sbnf1  34842  wl-mo2df  34857  wl-eudf  34859  wl-mo2t  34862  wl-mo3t  34863  wl-ax11-lem6  34873  wl-dfclab  34879  uncov  34924  tan2h  34935  matunitlindf  34941  ptrest  34942  poimirlem2  34945  poimirlem16  34959  poimirlem19  34962  poimirlem23  34966  poimirlem24  34967  poimirlem25  34968  poimirlem26  34969  poimirlem27  34970  mbfposadd  34990  cnambfre  34991  itg2addnclem2  34995  fdc  35069  heibor1  35134  rrncmslem  35156  rrnheibor  35161  opidonOLD  35176  issmgrpOLD  35187  ismndo  35196  isrngo  35221  isdivrngo  35274  isfldidl2  35393  isdmn3  35398  releleccnv  35564  releccnveq  35565  brcnvep  35572  elecres  35580  eleccnvep  35584  ideq2  35611  extid  35614  relcnveq3  35624  eqres  35643  brrabga  35644  ecin0  35652  alrmomodm  35659  brxrn  35672  brxrn2  35673  elecxrn  35684  br1cnvxrn2  35690  elec1cnvxrn2  35691  br1cossinres  35733  br1cossxrnres  35734  eldmcoss  35744  elrels2  35772  elrelscnveq3  35777  br1cnvssrres  35791  brcnvssr  35792  dfrefrels2  35799  dfcnvrefrels2  35812  dfsymrels2  35827  elrefsymrelsrel  35853  dftrrels2  35857  erim2  35957  eldisjs5  36005  prtlem13  36050  prter3  36064  lrelat  36196  islshpat  36199  lshpsmreu  36291  lkrpssN  36345  cmtvalN  36393  omllaw2N  36426  cvrval  36451  cvrval2  36456  cvlsupr3  36526  3dim0  36639  islln2  36693  islpln5  36717  islpln2  36718  islpln2ah  36731  islvol5  36761  islvol2  36762  4atlem11  36791  pmapglbx  36951  cdleme18d  37477  cdlemefrs29bpre0  37578  cdlemb3  37788  cdlemg33b  37889  cdlemkid3N  38115  cdlemkid4  38116  dvhb1dimN  38168  dia11N  38230  cdlemm10N  38300  dib11N  38342  dib1dim  38347  dibglbN  38348  diblsmopel  38353  dihopelvalcpre  38430  dih11  38447  dihmeetlem4preN  38488  dihmeetlem13N  38501  lcfrvalsnN  38723  lcfrlem9  38732  lcf1o  38733  mapdval4N  38814  baerlem3lem2  38892  baerlem5alem2  38893  baerlem5blem2  38894  hdmap1fval  38978  hdmapfval  39009  hdmapglem7a  39109  hlhillcs  39140  frlmfielbas  39269  addsubeq4com  39304  prjspreln0  39414  ellz1  39519  lzunuz  39520  fz1eqin  39521  diophrex  39527  rexrabdioph  39546  rexfrabdioph  39547  2rexfrabdioph  39548  3rexfrabdioph  39549  4rexfrabdioph  39550  6rexfrabdioph  39551  7rexfrabdioph  39552  fzneg  39734  expdioph  39775  wepwsolem  39797  fnwe2lem2  39806  islmodfg  39824  kercvrlsm  39838  cnvcnvintabd  40111  sqrtcvallem1  40142  iunrelexpuztr  40231  brtrclfv2  40239  frege124d  40273  rcompleq  40537  or3or  40538  uneqsn  40540  clsk1independent  40563  ntrclsneine0lem  40581  ntrclsiso  40584  ntrclsk2  40585  ntrclskb  40586  ntrclsk3  40587  ntrclsk13  40588  ntrclsk4  40589  ntrneiel2  40603  ntrneiiso  40608  ntrneikb  40611  ntrneik3  40613  ntrneix3  40614  ntrneik13  40615  ntrneix13  40616  ntrneik4w  40617  k0004lem3  40666  scottabf  40763  pm10.52  40884  iotasbc  40938  pm14.122a  40941  pm14.122b  40942  pm14.123a  40944  rusbcALT  40958  fvsb  40971  trsbc  41061  wessf1ornlem  41631  imassmpt  41723  limcperiod  42093  limsupre  42106  dvbdfbdioo  42395  stoweidlem34  42499  fourierdlem108  42679  fourierdlem110  42681  etransc  42748  funressnfv  43458  dfafn5a  43539  ndfatafv2nrn  43600  afv2ndefb  43603  dfatsnafv2  43631  dfatdmfcoafv2  43633  dfatco  43635  afv2fv0xorb  43646  readdcnnred  43683  resubcnnred  43684  recnmulnred  43685  cndivrenred  43686  elfz2z  43695  el1fzopredsuc  43705  elsetpreimafvb  43724  iccelpart  43773  ichan  43795  ichal  43806  reupr  43862  lighneallem2  43947  dfeven2  43990  gbowge7  44104  sbgoldbwt  44118  isupwlk  44187  uspgrsprfo  44199  ismhm0  44248  inclfusubc  44314  isrnghm  44339  rnghmval2  44342  uzlidlring  44376  lidldomnnring  44377  zrninitoringc  44518  opeliun2xp  44557  snlindsntor  44702  elbigo2  44788  0aryfvalel  44869  resum2sqorgt0  44934  rrx2pnedifcoorneor  44941  rrx2plord  44945  rrx2plordisom  44948  eenglngeehlnmlem1  44962  eenglngeehlnmlem2  44963  rrx2linest2  44969  itsclc0b  44997  itsclinecirc0in  45000  inlinecirc02plem  45011  gte-lte  45061  gt-lt  45062
  Copyright terms: Public domain W3C validator