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

Theorem syl6bbr 290
Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
syl6bbr.1 (𝜑 → (𝜓𝜒))
syl6bbr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6bbr (𝜑 → (𝜓𝜃))

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6bbr.2 . . 3 (𝜃𝜒)
32bicomi 225 . 2 (𝜒𝜃)
41, 3syl6bb 288 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:  3bitr4g  315  bibi2i  339  mtt  366  nbn2  372  ifptru  1065  3bior1fd  1466  3biant1d  1469  clelab  2955  eueq3  3699  n0moeu  4313  sbcel12  4357  sbceqg  4358  sbcne12  4361  reldisj  4398  raldifeq  4435  r19.3rz  4438  eldifpr  4587  reusngf  4604  rexreusng  4609  eldiftp  4616  reusv2lem5  5293  prelpw  5329  otthg  5368  2rbropap  5442  rabxp  5593  pwvrel  5595  elrng  5755  iss  5896  elimasni  5949  eliniseg  5951  idrefALT  5966  xpcan  6026  xpcan2  6027  elpredg  6155  ordelpss  6212  fcnvres  6549  dffv3  6659  funimass4  6723  unima  6732  fndmdif  6804  fneqeql  6808  funimass3  6816  elrnrexdmb  6848  dff4  6859  fnsnb  6920  fconst4  6968  elunirn  7001  f12dfv  7021  riota1  7124  riota2df  7126  f1ocnvfv3  7141  eqfnov  7269  elrnmpores  7277  caoftrn  7433  ordsucun  7529  dflim3  7551  dfom2  7571  peano5  7594  opiota  7746  suppssr  7850  mpoxopovel  7875  brtpos  7890  rntpos  7894  ordgt0ge1  8111  ondif2  8116  oelim2  8210  omabs  8263  iiner  8358  erinxp  8360  qliftfun  8371  mapdm0  8410  ordunifi  8756  elfi2  8866  elfiun  8882  fifo  8884  noinfep  9111  cantnflem1  9140  cantnf  9144  rankonidlem  9245  r1pwALT  9263  pr2nelem  9418  cardalephex  9504  alephinit  9509  dfac5lem4  9540  cflim2  9673  cfsmolem  9680  compssiso  9784  fin1a2lem11  9820  itunisuc  9829  axdclem  9929  brdom6disj  9942  alephreg  9992  fpwwe2lem9  10048  pwfseqlem3  10070  pwfseqlem4  10072  indpi  10317  nqereu  10339  ordpinq  10353  ltanq  10381  ltmnq  10382  suplem2pr  10463  map2psrpr  10520  ssxr  10698  leltne  10718  ltneg  11128  leneg  11131  suprnub  11594  negiso  11609  elnnnn0  11928  nn0sub  11935  zrevaddcl  12015  znnsub  12016  znn0sub  12017  prime  12051  eluz2  12237  indstr  12304  eluz2b1  12307  qrevaddcl  12358  rpneg  12409  xrleltne  12526  dfle2  12528  dflt2  12529  supxrleub  12707  infxrgelb  12716  ixxin  12743  iccid  12771  elicopnf  12821  iccsplit  12859  fzsplit2  12920  fzsn  12937  fzpr  12950  uzsplit  12967  preduz  13017  fvinim0ffz  13144  injresinj  13146  om2uzf1oi  13309  lt2sqi  13540  le2sqi  13541  hashsdom  13730  hashf1lem1  13801  fz1isolem  13807  prprrab  13819  ccatlcan  14068  ccatrcan  14069  s3eq3seq  14289  2swrd2eqwrdeq  14303  trclfvcotr  14357  cnpart  14587  limsuplt  14824  rlimresb  14910  mertenslem2  15229  fprod2dlem  15322  sadadd2lem2  15787  saddisjlem  15801  bitsuz  15811  gcddiv  15887  algcvgblem  15909  isprm3  16015  isprm5  16039  prmreclem5  16244  vdwapun  16298  vdwmc2  16303  ramcl  16353  pwsle  16753  ismre  16849  mreacs  16917  acsfn  16918  iscatd2  16940  cidpropd  16968  dfiso2  17030  oppcsect2  17037  isfunc  17122  setcinv  17338  lubeldm  17579  lubval  17582  glbeldm  17592  glbval  17595  tosso  17634  ipodrsfi  17761  acsfiindd  17775  imasmnd2  17936  resmndismnd  17961  submacs  17979  imasgrp2  18152  issubg  18217  resgrpisgrp  18238  subgacs  18251  eqgval  18267  gaorber  18376  symgfix2  18473  psgnran  18572  isslw  18662  sylow2alem2  18672  sylow2a  18673  sylow3lem6  18686  efgcpbllemb  18810  prmcyg  18943  gsum2d2lem  19022  gsumcom2  19024  subgdmdprd  19085  dprd2d2  19095  pgpfac1lem2  19126  pgpfac1lem4  19129  imasring  19298  drngmulne0  19453  subrgacs  19508  sdrgacs  19509  lssle0  19650  lssacs  19668  lssats2  19701  lvecvsn0  19810  islpir  19950  isnzr2  19964  zndvds  20624  znleval  20629  znleval2  20630  lindsmm  20900  islinds3  20906  islindf4  20910  eltg2b  21495  discld  21625  opnssneib  21651  cldlp  21686  restbas  21694  leordtvallem1  21746  leordtvallem2  21747  ssidcn  21791  cnprest2  21826  lmss  21834  perfcls  21901  cmpfi  21944  1stccnp  21998  subislly  22017  hausmapdom  22036  locfindis  22066  iskgen3  22085  kgencn  22092  ptpjpre1  22107  xkoccn  22155  txrest  22167  txlm  22184  txkgen  22188  xkopt  22191  xkoinjcn  22223  imasnopn  22226  imasncld  22227  imasncls  22228  qtopcn  22250  kqfeq  22260  isr0  22273  fbfinnfr  22377  trfbas  22380  fbunfip  22405  ufileu  22455  cfinufil  22464  fmid  22496  txflf  22542  fclsrest  22560  alexsubALT  22587  tsmsres  22679  ucnima  22817  fmucndlem  22827  bldisj  22935  xmeter  22970  elbl4  23100  restmetu  23107  dscopn  23110  bl2ioo  23327  isphtpc  23525  tcphcph  23767  lmmbr2  23789  lmmbrf  23792  iscau2  23807  iscauf  23810  caucfil  23813  metcld  23836  metcld2  23837  bcthlem1  23854  bcthlem4  23857  cldcss2  23972  ovolgelb  24008  ovoliunlem1  24030  ismbfcn  24157  mbfmax  24177  mbfimaopnlem  24183  i1faddlem  24221  i1fmullem  24222  i1fres  24233  i1fpos  24234  itg1climres  24242  xrge0f  24259  itgresr  24306  iblcnlem1  24315  limcun  24420  dvres  24436  mdegmullem  24599  ply1remlem  24683  plyremlem  24820  vieta1  24828  ulmcau  24910  sineq0  25036  coseq1  25037  ang180lem3  25316  cubic  25354  atandm  25381  atandm2  25382  atandm3  25383  rlimcnp  25470  rlimcnp2  25471  vmappw  25620  dchrelbas3  25741  dchrelbas4  25746  dchrsum2  25771  bposlem6  25792  2sqreuopltb  25968  2sqreuopnnltb  25970  dchrisumlem3  25994  pntleml  26114  istrkg3ld  26174  tgcgr4  26244  lnrot2  26337  islnopp  26452  islmib  26500  brbtwn2  26618  axsegconlem6  26635  axsegcon  26640  ax5seg  26651  axpasch  26654  axeuclid  26676  axcontlem4  26680  elntg2  26698  issubgr  26980  nb3gr2nb  27093  uhgrvd00  27243  isrusgr0  27275  wlkcpr  27337  wlkcomp  27339  upgr2wlk  27377  upgrf1istrl  27412  clwlkcomp  27487  clwlkcompbp  27490  iswwlksnx  27545  wspthsnwspthsnon  27622  wspniunwspnon  27629  2pthon3v  27649  usgr2wspthons3  27670  usgr2wspthon  27671  rusgrnumwwlks  27680  clwlkclwwlklem3  27706  clwlkclwwlk  27707  clwwlknonwwlknonb  27812  0pth  27831  eupth2lem2  27925  vdgn1frgrv2  28002  fusgreg2wsp  28042  clwwlknonclwlknonf1o  28068  dlwwlknondlwlknonf1o  28071  wlkl0  28073  nmoolb  28475  nmlno0lem  28497  ubthlem1  28574  ocsh  28987  shle0  29146  eigrei  29538  adjeu  29593  nmoplb  29611  nmfnlb  29628  eleigvec2  29662  nmlnop0iALT  29699  cnlnadjlem5  29775  adjbdln  29787  jplem2  29973  cvbr2  29987  mdsl2bi  30027  chrelat3  30075  sq2reunnltb  30175  rmounid  30186  eqsnd  30216  nelpr  30218  disjunsn  30272  ofpreima  30338  funcnvmpt  30340  funcnv5mpt  30341  dfcnv2  30350  gtiso  30362  fpwrelmap  30395  infxrge0glb  30415  xrdifh  30429  fzsplit3  30443  swrdrn3  30556  toslublem  30581  tosglblem  30583  xrge0tsmsbi  30620  cntzun  30622  isarchi  30738  isprmidl  30874  smatrcl  30960  unitdivcld  31043  lmxrge0  31094  isrrext  31140  issibf  31490  eulerpartlemr  31531  eulerpartlemmf  31532  eulerpartlemn  31538  dstfrvunirn  31631  ballotlemfc0  31649  ballotlemfcc  31650  reprsuc  31785  reprpmtf1o  31796  reprdifc  31797  bnj919  31937  bnj976  31948  bnj1542  32028  bnj150  32047  bnj151  32048  bnj607  32087  bnj852  32092  bnj873  32095  bnj938  32108  bnj1171  32169  bnj1388  32202  bnj1489  32225  usgrgt2cycl  32274  subfacp1lem3  32326  subfacp1lem5  32328  erdszelem9  32343  kur14  32360  iscvm  32403  satf0op  32521  mclsax  32713  dfpo2  32888  elintfv  32904  fundmpss  32906  opelco3  32915  dfon2  32934  noetalem3  33116  dfbigcup2  33257  sscoid  33271  funpartfv  33303  dfrdg4  33309  cgr3permute3  33405  segletr  33472  segleantisym  33473  seglelin  33474  fneval  33597  neibastop3  33607  eltail  33619  filnetlem4  33626  bj-hbntbi  33935  bj-sbceqgALT  34116  bj-rest10  34273  bj-0int  34287  bj-imdirid  34367  topdifinffinlem  34510  isbasisrelowllem1  34518  isbasisrelowllem2  34519  rdgeqoa  34533  finxpreclem4  34557  finxpsuclem  34560  uncf  34752  phpreu  34757  cos2h  34764  tan2h  34765  matunitlindflem1  34769  poimirlem16  34789  poimirlem19  34792  poimirlem23  34796  poimirlem24  34797  poimirlem26  34799  poimirlem27  34800  mbfposadd  34820  cnambfre  34821  itg2addnclem  34824  itg2addnc  34827  iblabsnclem  34836  ftc1anclem1  34848  ftc1anclem5  34852  caures  34916  heiborlem3  34972  heiborlem10  34979  elghomOLD  35046  divrngidl  35187  eqrelf  35398  brvbrvvdif  35406  eldmqsres2  35425  exanres  35433  ssrel3  35437  relcnveq  35460  iss2  35482  ecinn0  35488  brxrn2  35507  ecxrn  35519  eldmcoss2  35579  eldm1cossres  35580  elrelsrel  35607  elrelscnveq  35612  elcoeleqvrelsrel  35711  brredundsredund  35742  brdmqssqs  35762  cnvepresdmqss  35766  eldmqs1cossres  35773  brerser  35790  erim2  35791  eleldisjseldisj  35842  prtlem10  35881  prtlem16  35885  prtlem19  35894  prtex  35896  prter3  35898  islshpat  36033  lcvbr2  36038  lcvbr3  36039  lshpsmreu  36125  isat3  36323  hlrelat5N  36417  islpln5  36551  cdlemblem  36809  paddvaln0N  36817  paddval0  36826  cdlemefrs29bpre1  37413  cdlemefrs29cpre1  37414  cdlemg27b  37712  cdlemg33c  37724  cdlemg33e  37726  diaglbN  38071  cdlemm10N  38134  dicopelval2  38197  dicelval2N  38198  dihopelvalcpre  38264  dihglbcpreN  38316  dih1dimatlem  38345  dihatexv  38354  dvh4dimlem  38459  mapdpglem3  38691  hdmap14lem13  38896  hdmapglem7a  38943  fnsnbt  38998  isnacs2  39181  rabrenfdioph  39289  expdiophlem1  39496  pw2f1ocnv  39512  pwfi2f1o  39574  numinfctb  39581  dfacbasgrp  39586  islnr3  39593  isdomn3  39682  dfhe3  39999  clsk3nimkb  40268  ntrneiiso  40319  ntrneikb  40322  scottabf  40453  mnuunid  40490  hashnzfzclim  40531  dvconstbi  40543  sbcoreleleqVD  41070  rfcnpre3  41167  rfcnpre4  41168  cncfshift  42033  stoweidlem59  42221  dfafv23  43329  nelbrnel  43352  elsetpreimafvrab  43431  iccpartiun  43471  prproropf1olem0  43541  prprelb  43555  prprspr2  43557  reuprpr  43562  oddm1evenALTV  43717  oddp1evenALTV  43718  oddprmne2  43757  fpprel  43770  submgmacs  43948  ismhm0  43949  iscmgmALT  44059  iscsgrpALT  44061  isrnghmmul  44092  elpglem2  44742
  Copyright terms: Public domain W3C validator