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

Theorem syl6bbr 280
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 215 . 2 (𝜒𝜃)
41, 3syl6bb 278 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3bitr4g  305  bibi2i  328  mtt  355  nbn2  361  rbaibr  529  ifptru  1089  3bior1fd  1592  3biant1d  1595  clelab  2932  eueq3  3579  n0moeu  4138  sbcel12  4180  sbceqg  4181  sbcne12  4183  reldisj  4217  raldifeq  4254  r19.3rz  4257  eldifpr  4398  eldiftp  4420  reusv2lem5  5071  prelpw  5104  otthg  5143  2rbropap  5212  rabxp  5354  elrng  5515  iss  5652  elimasni  5702  eliniseg  5704  idrefALT  5719  xpcan  5781  xpcan2  5782  elpredg  5907  ordelpss  5964  fcnvres  6293  dffv3  6400  funimass4  6464  fndmdif  6539  fneqeql  6543  funimass3  6551  elrnrexdmb  6582  dff4  6591  fnsnb  6653  fconst4  6699  elunirn  6729  f12dfv  6749  riota1  6849  riota2df  6851  f1ocnvfv3  6866  eqfnov  6992  elrnmpt2res  7000  caoftrn  7158  ordsucun  7251  dflim3  7273  dfom2  7293  peano5  7315  opiota  7457  suppssr  7557  mpt2xopovel  7577  brtpos  7592  rntpos  7596  ordgt0ge1  7810  ondif2  7815  oelim2  7908  omabs  7960  iiner  8050  erinxp  8052  qliftfun  8063  mapdm0  8103  ordunifi  8445  elfi2  8555  elfiun  8571  fifo  8573  noinfep  8800  cantnflem1  8829  cantnf  8833  rankonidlem  8934  r1pwALT  8952  pr2nelem  9106  cardalephex  9192  alephinit  9197  dfac5lem4  9228  cflim2  9366  cfsmolem  9373  compssiso  9477  fin1a2lem11  9513  itunisuc  9522  axdclem  9622  brdom6disj  9635  alephreg  9685  fpwwe2lem9  9741  pwfseqlem3  9763  pwfseqlem4  9765  indpi  10010  nqereu  10032  ordpinq  10046  ltanq  10074  ltmnq  10075  suplem2pr  10156  map2psrpr  10212  ssxr  10388  letri3  10404  leltne  10408  ltneg  10809  leneg  10812  suprnub  11269  negiso  11284  elnnnn0  11598  nn0sub  11605  zrevaddcl  11684  znnsub  11685  znn0sub  11686  prime  11720  eluz2  11906  indstr  11971  eluz2b1  11974  qrevaddcl  12025  rpneg  12073  xrleltne  12190  dfle2  12192  dflt2  12193  xrletri3  12199  supxrleub  12370  infxrgelb  12379  ixxin  12406  iccid  12434  elicopnf  12484  iccsplit  12524  fzsplit2  12585  fzsn  12602  fzpr  12615  uzsplit  12631  preduz  12681  fvinim0ffz  12807  injresinj  12809  om2uzf1oi  12972  lt2sqi  13171  le2sqi  13172  hashsdom  13384  hashf1lem1  13452  fz1isolem  13458  prprrab  13468  ccatlcan  13692  ccatrcan  13693  s3eq3seq  13904  2swrd2eqwrdeq  13917  trclfvcotr  13969  cnpart  14199  limsuplt  14429  rlimresb  14515  mertenslem2  14834  fprod2dlem  14927  sadadd2lem2  15387  saddisjlem  15401  bitsuz  15411  gcddiv  15483  algcvgblem  15505  isprm3  15610  isprm5  15632  prmreclem5  15837  vdwapun  15891  vdwmc2  15896  ramcl  15946  pwsle  16353  ismre  16451  mreacs  16519  acsfn  16520  iscatd2  16542  cidpropd  16570  dfiso2  16632  oppcsect2  16639  isfunc  16724  setcinv  16940  lubeldm  17182  lubval  17185  glbeldm  17195  glbval  17198  tosso  17237  ipodrsfi  17364  acsfiindd  17378  imasmnd2  17528  submacs  17566  imasgrp2  17731  issubg  17792  resgrpisgrp  17813  subgacs  17827  eqgval  17841  gaorber  17938  symgfix2  18033  psgnran  18132  isslw  18220  sylow2alem2  18230  sylow2a  18231  sylow3lem6  18244  efgcpbllemb  18365  prmcyg  18492  gsum2d2lem  18569  gsumcom2  18571  subgdmdprd  18631  dprd2d2  18641  pgpfac1lem2  18672  pgpfac1lem4  18675  imasring  18817  drngmulne0  18969  lssle0  19150  lssacs  19170  lssats2  19203  lvecvsn0  19312  islpir  19454  isnzr2  19468  zndvds  20101  znleval  20106  znleval2  20107  lindsmm  20373  islinds3  20379  islindf4  20383  eltg2b  20973  discld  21103  opnssneib  21129  cldlp  21164  restbas  21172  leordtvallem1  21224  leordtvallem2  21225  ssidcn  21269  cnprest2  21304  lmss  21312  perfcls  21379  cmpfi  21421  1stccnp  21475  subislly  21494  hausmapdom  21513  locfindis  21543  iskgen3  21562  kgencn  21569  ptpjpre1  21584  xkoccn  21632  txrest  21644  txlm  21661  txkgen  21665  xkopt  21668  xkoinjcn  21700  imasnopn  21703  imasncld  21704  imasncls  21705  qtopcn  21727  kqfeq  21737  isr0  21750  fbfinnfr  21854  trfbas  21857  fbunfip  21882  ufileu  21932  cfinufil  21941  fmid  21973  txflf  22019  fclsrest  22037  alexsubALT  22064  tsmsres  22156  ucnima  22294  fmucndlem  22304  bldisj  22412  xmeter  22447  elbl4  22577  restmetu  22584  dscopn  22587  bl2ioo  22804  isphtpc  23002  tchcph  23244  lmmbr2  23265  lmmbrf  23268  iscau2  23283  iscauf  23286  caucfil  23289  metcld  23312  metcld2  23313  bcthlem1  23329  bcthlem4  23332  cldcss2  23421  ovolgelb  23457  ovoliunlem1  23479  ismbfcn  23606  mbfmax  23626  mbfimaopnlem  23632  i1faddlem  23670  i1fmullem  23671  i1fres  23682  i1fpos  23683  itg1climres  23691  xrge0f  23708  itgresr  23755  iblcnlem1  23764  limcun  23869  dvres  23885  mdegmullem  24048  ply1remlem  24132  plyremlem  24269  vieta1  24277  ulmcau  24359  sineq0  24484  coseq1  24485  ang180lem3  24751  cubic  24786  atandm  24813  atandm2  24814  atandm3  24815  rlimcnp  24902  rlimcnp2  24903  vmappw  25052  dchrelbas3  25173  dchrelbas4  25178  dchrsum2  25203  bposlem6  25224  dchrisumlem3  25390  pntleml  25510  istrkg3ld  25570  tgcgr4  25636  lnrot2  25729  islnopp  25841  islmib  25889  brbtwn2  25995  axsegconlem6  26012  axsegcon  26017  ax5seg  26028  axpasch  26031  axeuclid  26053  axcontlem4  26057  issubgr  26375  nb3gr2nb  26498  uhgrvd00  26654  isrusgr0  26686  wlkcpr  26748  wlkcomp  26750  upgr2wlk  26788  upgrf1istrl  26824  clwlkcomp  26899  clwlkcompbp  26902  iswwlksnx  26957  wspthsnwspthsnon  27050  wspthsnwspthsnonOLD  27052  wspniunwspnon  27059  2pthon3v  27079  usgr2wspthons3  27102  usgr2wspthon  27103  rusgrnumwwlks  27112  clwlkclwwlklem3  27140  clwlkclwwlk  27141  clwwlknonelOLD  27259  0pth  27294  eupth2lem2  27388  vdgn1frgrv2  27467  fusgreg2wsp  27507  numclwwlkovgelOLD  27525  clwwlknonclwlknonf1o  27538  dlwwlknondlwlknonf1o  27541  wlkl0  27543  nmoolb  27950  nmlno0lem  27972  ubthlem1  28050  ocsh  28466  shle0  28625  eigrei  29017  adjeu  29072  nmoplb  29090  nmfnlb  29107  eleigvec2  29141  nmlnop0iALT  29178  cnlnadjlem5  29254  adjbdln  29266  jplem2  29452  cvbr2  29466  mdsl2bi  29506  chrelat3  29554  disjunsn  29728  ofpreima  29788  funcnvmpt  29791  funcnv5mpt  29792  dfcnv2  29799  gtiso  29801  fpwrelmap  29831  infxrge0glb  29853  xrdifh  29865  fzsplit3  29876  toslublem  29988  tosglblem  29990  isarchi  30057  xrge0tsmsbi  30107  smatrcl  30183  unitdivcld  30268  lmxrge0  30319  isrrext  30365  issibf  30716  eulerpartlemr  30757  eulerpartlemmf  30758  eulerpartlemn  30764  dstfrvunirn  30857  ballotlemfc0  30875  ballotlemfcc  30876  reprsuc  31014  reprpmtf1o  31025  reprdifc  31026  bnj919  31155  bnj976  31166  bnj1542  31245  bnj150  31264  bnj151  31265  bnj607  31304  bnj852  31309  bnj873  31312  bnj938  31325  bnj1171  31386  bnj1388  31419  bnj1489  31442  subfacp1lem3  31482  subfacp1lem5  31484  erdszelem9  31499  kur14  31516  iscvm  31559  mclsax  31784  dfpo2  31962  elintfv  31979  fundmpss  31981  opelco3  31993  dfon2  32012  noetalem3  32181  dfbigcup2  32322  sscoid  32336  funpartfv  32368  dfrdg4  32374  cgr3permute3  32470  segletr  32537  segleantisym  32538  seglelin  32539  fneval  32663  neibastop3  32673  eltail  32685  filnetlem4  32692  bj-hbntbi  33005  bj-sbceqgALT  33200  bj-rest10  33347  bj-0int  33361  topdifinffinlem  33506  isbasisrelowllem1  33514  isbasisrelowllem2  33515  rdgeqoa  33529  finxpreclem4  33542  finxpsuclem  33545  uncf  33696  phpreu  33701  cos2h  33708  tan2h  33709  matunitlindflem1  33713  poimirlem16  33733  poimirlem19  33736  poimirlem23  33740  poimirlem24  33741  poimirlem26  33743  poimirlem27  33744  mbfposadd  33764  cnambfre  33765  itg2addnclem  33768  itg2addnc  33771  iblabsnclem  33780  ftc1anclem1  33792  ftc1anclem5  33796  caures  33862  heiborlem3  33918  heiborlem10  33925  elghomOLD  33992  divrngidl  34133  eqrelf  34333  brvbrvvdif  34341  eldmqsres2  34364  exanres  34375  ssrel3  34379  relcnveq  34403  iss2  34420  ecinn0  34426  brxrn2  34445  ecxrn  34457  eldmcoss2  34517  eldm1cossres  34518  elrelsrel  34545  elrelscnveq  34550  prtlem10  34639  prtlem16  34643  prtlem19  34652  prtex  34654  prter3  34656  islshpat  34792  lcvbr2  34797  lcvbr3  34798  lshpsmreu  34884  isat3  35082  hlrelat5N  35176  islpln5  35310  cdlemblem  35568  paddvaln0N  35576  paddval0  35585  cdlemefrs29bpre1  36172  cdlemefrs29cpre1  36173  cdlemg27b  36471  cdlemg33c  36483  cdlemg33e  36485  diaglbN  36830  cdlemm10N  36893  dicopelval2  36956  dicelval2N  36957  dihopelvalcpre  37023  dihglbcpreN  37075  dih1dimatlem  37104  dihatexv  37113  dvh4dimlem  37218  mapdpglem3  37450  hdmap14lem13  37655  hdmapglem7a  37702  isnacs2  37765  rabrenfdioph  37874  expdiophlem1  38083  pw2f1ocnv  38099  pwfi2f1o  38161  numinfctb  38168  dfacbasgrp  38173  islnr3  38180  subrgacs  38265  sdrgacs  38266  isdomn3  38277  dfhe3  38563  clsk3nimkb  38832  ntrneiiso  38883  ntrneikb  38886  hashnzfzclim  39015  dvconstbi  39027  sbc3orgOLD  39234  sbcel12gOLD  39246  rfcnpre3  39680  rfcnpre4  39681  unima  39829  cncfshift  40561  stoweidlem59  40749  dfafv23  41836  nelbrnel  41859  iccpartiun  41939  oddm1evenALTV  42155  oddp1evenALTV  42156  oddprmne2  42193  submgmacs  42366  ismhm0  42367  iscmgmALT  42422  iscsgrpALT  42424  isrnghmmul  42455  elpglem2  43020
  Copyright terms: Public domain W3C validator