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

Theorem syl6bbr 278
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 214 . 2 (𝜒𝜃)
41, 3syl6bb 276 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:  3bitr4g  303  bibi2i  327  mtt  354  nbn2  360  rbaibr  945  ifptru  1022  3bior1fd  1436  3biant1d  1439  clelab  2746  eueq3  3375  n0moeu  3929  sbcel12  3974  sbceqg  3975  sbcne12  3977  reldisj  4011  raldifeq  4050  r19.3rz  4053  eldifpr  4195  eldiftp  4219  reusv2lem5  4864  prelpw  4905  otthg  4944  2rbropap  5007  rabxp  5144  elrng  5303  iss  5435  elimasni  5480  eliniseg  5482  xpcan  5558  xpcan2  5559  elpredg  5682  ordelpss  5739  fcnvres  6069  dffv3  6174  funimass4  6234  fndmdif  6307  fneqeql  6311  funimass3  6319  elrnrexdmb  6350  dff4  6359  fnsnb  6417  fconst4  6463  elunirn  6494  f12dfv  6514  riota1  6614  riota2df  6616  f1ocnvfv3  6631  eqfnov  6751  elrnmpt2res  6759  caoftrn  6917  ordsucun  7010  dflim3  7032  dfom2  7052  peano5  7074  opiota  7214  suppssr  7311  mpt2xopovel  7331  brtpos  7346  rntpos  7350  ordgt0ge1  7562  ondif2  7567  oelim2  7660  omabs  7712  iiner  7804  erinxp  7806  qliftfun  7817  mapdm0  7857  ordunifi  8195  elfi2  8305  elfiun  8321  fifo  8323  noinfep  8542  cantnflem1  8571  cantnf  8575  rankonidlem  8676  r1pwALT  8694  pr2nelem  8812  cardalephex  8898  alephinit  8903  dfac5lem4  8934  cflim2  9070  cfsmolem  9077  compssiso  9181  fin1a2lem11  9217  itunisuc  9226  axdclem  9326  brdom6disj  9339  alephreg  9389  fpwwe2lem9  9445  pwfseqlem3  9467  pwfseqlem4  9469  indpi  9714  nqereu  9736  ordpinq  9750  ltanq  9778  ltmnq  9779  suplem2pr  9860  map2psrpr  9916  ssxr  10092  letri3  10108  leltne  10112  ltneg  10513  leneg  10516  suprnub  10973  negiso  10988  elnnnn0  11321  nn0sub  11328  zrevaddcl  11407  znnsub  11408  znn0sub  11409  prime  11443  eluz2  11678  indstr  11741  eluz2b1  11744  qrevaddcl  11795  rpneg  11848  xrleltne  11963  dfle2  11965  dflt2  11966  xrletri3  11970  supxrleub  12141  infxrgelb  12150  ixxin  12177  iccid  12205  elicopnf  12254  iccsplit  12290  fzsplit2  12351  fzsn  12368  fzpr  12381  uzsplit  12396  preduz  12445  fvinim0ffz  12570  injresinj  12572  om2uzf1oi  12735  lt2sqi  12935  le2sqi  12936  hashsdom  13153  hashf1lem1  13222  fz1isolem  13228  prprrab  13238  ccatlcan  13454  ccatrcan  13455  s3eq3seq  13665  2swrd2eqwrdeq  13677  trclfvcotr  13731  cnpart  13961  limsuplt  14191  rlimresb  14277  mertenslem2  14598  fprod2dlem  14691  sadadd2lem2  15153  saddisjlem  15167  bitsuz  15177  gcddiv  15249  algcvgblem  15271  isprm2lem  15375  isprm3  15377  isprm5  15400  prmreclem5  15605  vdwapun  15659  vdwmc2  15664  ramcl  15714  pwsle  16133  ismre  16231  mreacs  16300  acsfn  16301  iscatd2  16323  cidpropd  16351  dfiso2  16413  oppcsect2  16420  isfunc  16505  setcinv  16721  lubeldm  16962  lubval  16965  glbeldm  16975  glbval  16978  tosso  17017  ipodrsfi  17144  acsfiindd  17158  imasmnd2  17308  submacs  17346  imasgrp2  17511  issubg  17575  resgrpisgrp  17596  subgacs  17610  eqgval  17624  gaorber  17722  symgfix2  17817  psgnran  17916  isslw  18004  sylow2alem2  18014  sylow2a  18015  sylow3lem6  18028  efgcpbllemb  18149  prmcyg  18276  gsum2d2lem  18353  gsumcom2  18355  subgdmdprd  18414  dprd2d2  18424  pgpfac1lem2  18455  pgpfac1lem4  18458  imasring  18600  drngmulne0  18750  lssle0  18931  lssacs  18948  lssats2  18981  lvecvsn0  19090  islpir  19230  isnzr2  19244  zndvds  19879  znleval  19884  znleval2  19885  lindsmm  20148  islinds3  20154  islindf4  20158  eltg2b  20744  discld  20874  opnssneib  20900  cldlp  20935  restbas  20943  leordtvallem1  20995  leordtvallem2  20996  ssidcn  21040  cnprest2  21075  lmss  21083  perfcls  21150  cmpfi  21192  1stccnp  21246  subislly  21265  hausmapdom  21284  locfindis  21314  iskgen3  21333  kgencn  21340  ptpjpre1  21355  xkoccn  21403  txrest  21415  txlm  21432  txkgen  21436  xkopt  21439  xkoinjcn  21471  imasnopn  21474  imasncld  21475  imasncls  21476  qtopcn  21498  kqfeq  21508  isr0  21521  fbfinnfr  21626  trfbas  21629  fbunfip  21654  ufileu  21704  cfinufil  21713  fmid  21745  txflf  21791  fclsrest  21809  alexsubALT  21836  tsmsres  21928  ucnima  22066  fmucndlem  22076  bldisj  22184  xmeter  22219  elbl4  22349  restmetu  22356  dscopn  22359  bl2ioo  22576  isphtpc  22774  tchcph  23017  lmmbr2  23038  lmmbrf  23041  iscau2  23056  iscauf  23059  caucfil  23062  metcld  23085  metcld2  23086  bcthlem1  23102  bcthlem4  23105  cldcss2  23194  ovolgelb  23229  ovoliunlem1  23251  ismbfcn  23379  mbfmax  23397  mbfimaopnlem  23403  i1faddlem  23441  i1fmullem  23442  i1fres  23453  i1fpos  23454  itg1climres  23462  xrge0f  23479  itgresr  23526  iblcnlem1  23535  limcun  23640  dvres  23656  mdegmullem  23819  ply1remlem  23903  plyremlem  24040  vieta1  24048  ulmcau  24130  sineq0  24254  coseq1  24255  ang180lem3  24522  cubic  24557  atandm  24584  atandm2  24585  atandm3  24586  rlimcnp  24673  rlimcnp2  24674  vmappw  24823  dchrelbas3  24944  dchrelbas4  24949  dchrsum2  24974  bposlem6  24995  dchrisumlem3  25161  pntleml  25281  istrkg3ld  25341  tgcgr4  25407  lnrot2  25500  islnopp  25612  islmib  25660  brbtwn2  25766  axsegconlem6  25783  axsegcon  25788  ax5seg  25799  axpasch  25802  axeuclid  25824  axcontlem4  25828  issubgr  26144  nb3gr2nb  26267  uhgrvd00  26411  isrusgr0  26443  wlkcpr  26505  wlkcomp  26507  upgr2wlk  26545  upgrf1istrl  26581  clwlkcomp  26656  iswwlksnx  26712  wspthsnwspthsnon  26792  wspniunwspnon  26800  2pthon3v  26820  usgr2wspthons3  26838  usgr2wspthon  26839  rusgrnumwwlks  26850  clwlkclwwlklem3  26883  clwlkclwwlk  26884  0pth  26966  eupth2lem2  27059  vdgn1frgrv2  27140  fusgreg2wsp  27174  numclwwlkovgel  27193  nmoolb  27596  nmlno0lem  27618  ubthlem1  27696  ocsh  28112  shle0  28271  eigrei  28663  adjeu  28718  nmoplb  28736  nmfnlb  28753  eleigvec2  28787  nmlnop0iALT  28824  cnlnadjlem5  28900  adjbdln  28912  jplem2  29098  cvbr2  29112  mdsl2bi  29152  chrelat3  29200  disjunsn  29379  ofpreima  29439  funcnvmpt  29442  funcnv5mpt  29443  dfcnv2  29450  gtiso  29452  fpwrelmap  29482  infxrge0glb  29504  xrdifh  29516  fzsplit3  29527  toslublem  29641  tosglblem  29643  isarchi  29710  xrge0tsmsbi  29760  smatrcl  29836  unitdivcld  29921  lmxrge0  29972  isrrext  30018  issibf  30369  eulerpartlemr  30410  eulerpartlemmf  30411  eulerpartlemn  30417  dstfrvunirn  30510  ballotlemfc0  30528  ballotlemfcc  30529  reprsuc  30667  reprpmtf1o  30678  reprdifc  30679  bnj919  30811  bnj976  30822  bnj1542  30901  bnj150  30920  bnj151  30921  bnj607  30960  bnj852  30965  bnj873  30968  bnj938  30981  bnj1171  31042  bnj1388  31075  bnj1489  31098  subfacp1lem3  31138  subfacp1lem5  31140  erdszelem9  31155  kur14  31172  iscvm  31215  mclsax  31440  dfpo2  31620  elintfv  31638  fundmpss  31640  opelco3  31652  dfon2  31671  noetalem3  31839  dfbigcup2  31981  sscoid  31995  funpartfv  32027  dfrdg4  32033  cgr3permute3  32129  segletr  32196  segleantisym  32197  seglelin  32198  fneval  32322  neibastop3  32332  eltail  32344  filnetlem4  32351  bj-hbntbi  32670  bj-sbceqgALT  32872  bj-rest10  33016  bj-0int  33030  topdifinffinlem  33166  isbasisrelowllem1  33174  isbasisrelowllem2  33175  rdgeqoa  33189  finxpreclem4  33202  finxpsuclem  33205  uncf  33359  phpreu  33364  cos2h  33371  tan2h  33372  matunitlindflem1  33376  poimirlem16  33396  poimirlem19  33399  poimirlem23  33403  poimirlem24  33404  poimirlem26  33406  poimirlem27  33407  mbfposadd  33428  cnambfre  33429  itg2addnclem  33432  itg2addnc  33435  iblabsnclem  33444  ftc1anclem1  33456  ftc1anclem5  33460  caures  33527  heiborlem3  33583  heiborlem10  33590  elghomOLD  33657  divrngidl  33798  prtlem10  33969  prtlem16  33973  prtlem19  33982  prtex  33984  prter3  33986  islshpat  34123  lcvbr2  34128  lcvbr3  34129  lshpsmreu  34215  isat3  34413  hlrelat5N  34506  islpln5  34640  cdlemblem  34898  paddvaln0N  34906  paddval0  34915  cdlemefrs29bpre1  35504  cdlemefrs29cpre1  35505  cdlemg27b  35803  cdlemg33c  35815  cdlemg33e  35817  diaglbN  36163  cdlemm10N  36226  dicopelval2  36289  dicelval2N  36290  dihopelvalcpre  36356  dihglbcpreN  36408  dih1dimatlem  36437  dihatexv  36446  dvh4dimlem  36551  mapdpglem3  36783  hdmap14lem13  36991  hdmapglem7a  37038  isnacs2  37088  rabrenfdioph  37197  expdiophlem1  37407  pw2f1ocnv  37423  pwfi2f1o  37485  numinfctb  37492  dfacbasgrp  37497  islnr3  37504  subrgacs  37589  sdrgacs  37590  isdomn3  37601  dfhe3  37889  clsk3nimkb  38158  ntrneiiso  38209  ntrneikb  38212  hashnzfzclim  38341  dvconstbi  38353  sbc3orgOLD  38562  sbcel12gOLD  38574  sbcssOLD  38576  rfcnpre3  39012  rfcnpre4  39013  unima  39162  cncfshift  39850  stoweidlem59  40039  nelbrnel  41056  iccpartiun  41134  oddm1evenALTV  41351  oddp1evenALTV  41352  oddprmne2  41389  submgmacs  41569  ismhm0  41570  iscmgmALT  41625  iscsgrpALT  41627  isrnghmmul  41658  elpglem2  42220
  Copyright terms: Public domain W3C validator