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  326  mtt  353  nbn2  359  rbaibr  519  ifptru  1059  3bior1fd  1585  3biant1d  1588  clelab  2896  eueq3  3531  n0moeu  4082  sbcel12  4125  sbceqg  4126  sbcne12  4128  reldisj  4161  raldifeq  4198  r19.3rz  4201  eldifpr  4341  eldiftp  4363  reusv2lem5  5001  prelpw  5042  otthg  5081  2rbropap  5150  rabxp  5294  elrng  5452  iss  5588  elimasni  5633  eliniseg  5635  xpcan  5711  xpcan2  5712  elpredg  5837  ordelpss  5894  fcnvres  6222  dffv3  6328  funimass4  6389  fndmdif  6464  fneqeql  6468  funimass3  6476  elrnrexdmb  6507  dff4  6516  fnsnb  6575  fconst4  6621  elunirn  6651  f12dfv  6671  riota1  6771  riota2df  6773  f1ocnvfv3  6788  eqfnov  6912  elrnmpt2res  6920  caoftrn  7078  ordsucun  7171  dflim3  7193  dfom2  7213  peano5  7235  opiota  7377  suppssr  7477  mpt2xopovel  7497  brtpos  7512  rntpos  7516  ordgt0ge1  7730  ondif2  7735  oelim2  7828  omabs  7880  iiner  7970  erinxp  7972  qliftfun  7983  mapdm0  8023  ordunifi  8365  elfi2  8475  elfiun  8491  fifo  8493  noinfep  8720  cantnflem1  8749  cantnf  8753  rankonidlem  8854  r1pwALT  8872  pr2nelem  9026  cardalephex  9112  alephinit  9117  dfac5lem4  9148  cflim2  9286  cfsmolem  9293  compssiso  9397  fin1a2lem11  9433  itunisuc  9442  axdclem  9542  brdom6disj  9555  alephreg  9605  fpwwe2lem9  9661  pwfseqlem3  9683  pwfseqlem4  9685  indpi  9930  nqereu  9952  ordpinq  9966  ltanq  9994  ltmnq  9995  suplem2pr  10076  map2psrpr  10132  ssxr  10308  letri3  10324  leltne  10328  ltneg  10729  leneg  10732  suprnub  11189  negiso  11204  elnnnn0  11537  nn0sub  11544  zrevaddcl  11623  znnsub  11624  znn0sub  11625  prime  11659  eluz2  11893  indstr  11958  eluz2b1  11961  qrevaddcl  12012  rpneg  12065  xrleltne  12182  dfle2  12184  dflt2  12185  xrletri3  12189  supxrleub  12360  infxrgelb  12369  ixxin  12396  iccid  12424  elicopnf  12474  iccsplit  12511  fzsplit2  12572  fzsn  12589  fzpr  12602  uzsplit  12618  preduz  12668  fvinim0ffz  12794  injresinj  12796  om2uzf1oi  12959  lt2sqi  13158  le2sqi  13159  hashsdom  13371  hashf1lem1  13440  fz1isolem  13446  prprrab  13456  ccatlcan  13680  ccatrcan  13681  s3eq3seq  13892  2swrd2eqwrdeq  13905  trclfvcotr  13957  cnpart  14187  limsuplt  14417  rlimresb  14503  mertenslem2  14823  fprod2dlem  14916  sadadd2lem2  15379  saddisjlem  15393  bitsuz  15403  gcddiv  15475  algcvgblem  15497  isprm3  15602  isprm5  15625  prmreclem5  15830  vdwapun  15884  vdwmc2  15889  ramcl  15939  pwsle  16359  ismre  16457  mreacs  16525  acsfn  16526  iscatd2  16548  cidpropd  16576  dfiso2  16638  oppcsect2  16645  isfunc  16730  setcinv  16946  lubeldm  17188  lubval  17191  glbeldm  17201  glbval  17204  tosso  17243  ipodrsfi  17370  acsfiindd  17384  imasmnd2  17534  submacs  17572  imasgrp2  17737  issubg  17801  resgrpisgrp  17822  subgacs  17836  eqgval  17850  gaorber  17947  symgfix2  18042  psgnran  18141  isslw  18229  sylow2alem2  18239  sylow2a  18240  sylow3lem6  18253  efgcpbllemb  18374  prmcyg  18501  gsum2d2lem  18578  gsumcom2  18580  subgdmdprd  18640  dprd2d2  18650  pgpfac1lem2  18681  pgpfac1lem4  18684  imasring  18826  drngmulne0  18978  lssle0  19159  lssacs  19179  lssats2  19212  lvecvsn0  19321  islpir  19463  isnzr2  19477  zndvds  20112  znleval  20117  znleval2  20118  lindsmm  20383  islinds3  20389  islindf4  20393  eltg2b  20983  discld  21113  opnssneib  21139  cldlp  21174  restbas  21182  leordtvallem1  21234  leordtvallem2  21235  ssidcn  21279  cnprest2  21314  lmss  21322  perfcls  21389  cmpfi  21431  1stccnp  21485  subislly  21504  hausmapdom  21523  locfindis  21553  iskgen3  21572  kgencn  21579  ptpjpre1  21594  xkoccn  21642  txrest  21654  txlm  21671  txkgen  21675  xkopt  21678  xkoinjcn  21710  imasnopn  21713  imasncld  21714  imasncls  21715  qtopcn  21737  kqfeq  21747  isr0  21760  fbfinnfr  21864  trfbas  21867  fbunfip  21892  ufileu  21942  cfinufil  21951  fmid  21983  txflf  22029  fclsrest  22047  alexsubALT  22074  tsmsres  22166  ucnima  22304  fmucndlem  22314  bldisj  22422  xmeter  22457  elbl4  22587  restmetu  22594  dscopn  22597  bl2ioo  22814  isphtpc  23012  tchcph  23254  lmmbr2  23275  lmmbrf  23278  iscau2  23293  iscauf  23296  caucfil  23299  metcld  23322  metcld2  23323  bcthlem1  23339  bcthlem4  23342  cldcss2  23431  ovolgelb  23467  ovoliunlem1  23489  ismbfcn  23616  mbfmax  23635  mbfimaopnlem  23641  i1faddlem  23679  i1fmullem  23680  i1fres  23691  i1fpos  23692  itg1climres  23700  xrge0f  23717  itgresr  23764  iblcnlem1  23773  limcun  23878  dvres  23894  mdegmullem  24057  ply1remlem  24141  plyremlem  24278  vieta1  24286  ulmcau  24368  sineq0  24493  coseq1  24494  ang180lem3  24761  cubic  24796  atandm  24823  atandm2  24824  atandm3  24825  rlimcnp  24912  rlimcnp2  24913  vmappw  25062  dchrelbas3  25183  dchrelbas4  25188  dchrsum2  25213  bposlem6  25234  dchrisumlem3  25400  pntleml  25520  istrkg3ld  25580  tgcgr4  25646  lnrot2  25739  islnopp  25851  islmib  25899  brbtwn2  26005  axsegconlem6  26022  axsegcon  26027  ax5seg  26038  axpasch  26041  axeuclid  26063  axcontlem4  26067  issubgr  26385  nb3gr2nb  26508  uhgrvd00  26664  isrusgr0  26696  wlkcpr  26758  wlkcomp  26760  upgr2wlk  26798  upgrf1istrl  26834  clwlkcomp  26909  clwlkcompbp  26912  iswwlksnx  26967  wspthsnwspthsnon  27058  wspthsnwspthsnonOLD  27060  wspniunwspnon  27067  2pthon3v  27087  usgr2wspthons3  27110  usgr2wspthon  27111  rusgrnumwwlks  27120  clwlkclwwlklem3  27148  clwlkclwwlk  27149  clwwlknonelOLD  27267  0pth  27302  eupth2lem2  27396  vdgn1frgrv2  27475  fusgreg2wsp  27515  numclwwlkovgelOLD  27534  wlkl0  27553  nmoolb  27960  nmlno0lem  27982  ubthlem1  28060  ocsh  28476  shle0  28635  eigrei  29027  adjeu  29082  nmoplb  29100  nmfnlb  29117  eleigvec2  29151  nmlnop0iALT  29188  cnlnadjlem5  29264  adjbdln  29276  jplem2  29462  cvbr2  29476  mdsl2bi  29516  chrelat3  29564  disjunsn  29739  ofpreima  29799  funcnvmpt  29802  funcnv5mpt  29803  dfcnv2  29810  gtiso  29812  fpwrelmap  29842  infxrge0glb  29864  xrdifh  29876  fzsplit3  29887  toslublem  30001  tosglblem  30003  isarchi  30070  xrge0tsmsbi  30120  smatrcl  30196  unitdivcld  30281  lmxrge0  30332  isrrext  30378  issibf  30729  eulerpartlemr  30770  eulerpartlemmf  30771  eulerpartlemn  30777  dstfrvunirn  30870  ballotlemfc0  30888  ballotlemfcc  30889  reprsuc  31027  reprpmtf1o  31038  reprdifc  31039  bnj919  31169  bnj976  31180  bnj1542  31259  bnj150  31278  bnj151  31279  bnj607  31318  bnj852  31323  bnj873  31326  bnj938  31339  bnj1171  31400  bnj1388  31433  bnj1489  31456  subfacp1lem3  31496  subfacp1lem5  31498  erdszelem9  31513  kur14  31530  iscvm  31573  mclsax  31798  dfpo2  31977  elintfv  31994  fundmpss  31996  opelco3  32008  dfon2  32027  noetalem3  32196  dfbigcup2  32337  sscoid  32351  funpartfv  32383  dfrdg4  32389  cgr3permute3  32485  segletr  32552  segleantisym  32553  seglelin  32554  fneval  32678  neibastop3  32688  eltail  32700  filnetlem4  32707  bj-hbntbi  33026  bj-sbceqgALT  33220  bj-rest10  33366  bj-0int  33380  topdifinffinlem  33525  isbasisrelowllem1  33533  isbasisrelowllem2  33534  rdgeqoa  33548  finxpreclem4  33561  finxpsuclem  33564  uncf  33714  phpreu  33719  cos2h  33726  tan2h  33727  matunitlindflem1  33731  poimirlem16  33751  poimirlem19  33754  poimirlem23  33758  poimirlem24  33759  poimirlem26  33761  poimirlem27  33762  mbfposadd  33782  cnambfre  33783  itg2addnclem  33786  itg2addnc  33789  iblabsnclem  33798  ftc1anclem1  33810  ftc1anclem5  33814  caures  33881  heiborlem3  33937  heiborlem10  33944  elghomOLD  34011  divrngidl  34152  eqrelf  34356  brvbrvvdif  34364  eldmqsres2  34388  exanres  34399  ssrel3  34403  relcnveq  34429  iss2  34447  ecinn0  34453  brxrn2  34472  ecxrn  34484  eldmcoss2  34544  eldm1cossres  34545  elrelsrel  34572  elrelscnveq  34577  prtlem10  34666  prtlem16  34670  prtlem19  34679  prtex  34681  prter3  34683  islshpat  34819  lcvbr2  34824  lcvbr3  34825  lshpsmreu  34911  isat3  35109  hlrelat5N  35202  islpln5  35336  cdlemblem  35594  paddvaln0N  35602  paddval0  35611  cdlemefrs29bpre1  36199  cdlemefrs29cpre1  36200  cdlemg27b  36498  cdlemg33c  36510  cdlemg33e  36512  diaglbN  36858  cdlemm10N  36921  dicopelval2  36984  dicelval2N  36985  dihopelvalcpre  37051  dihglbcpreN  37103  dih1dimatlem  37132  dihatexv  37141  dvh4dimlem  37246  mapdpglem3  37478  hdmap14lem13  37683  hdmapglem7a  37730  isnacs2  37788  rabrenfdioph  37897  expdiophlem1  38107  pw2f1ocnv  38123  pwfi2f1o  38185  numinfctb  38192  dfacbasgrp  38197  islnr3  38204  subrgacs  38289  sdrgacs  38290  isdomn3  38301  dfhe3  38588  clsk3nimkb  38857  ntrneiiso  38908  ntrneikb  38911  hashnzfzclim  39040  dvconstbi  39052  sbc3orgOLD  39261  sbcel12gOLD  39273  rfcnpre3  39708  rfcnpre4  39709  unima  39860  cncfshift  40599  stoweidlem59  40787  nelbrnel  41810  iccpartiun  41888  oddm1evenALTV  42104  oddp1evenALTV  42105  oddprmne2  42142  submgmacs  42322  ismhm0  42323  iscmgmALT  42378  iscsgrpALT  42380  isrnghmmul  42411  elpglem2  42976
  Copyright terms: Public domain W3C validator