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  966  ifptru  1043  3bior1fd  1478  3biant1d  1481  clelab  2777  eueq3  3414  n0moeu  3970  sbcel12  4016  sbceqg  4017  sbcne12  4019  reldisj  4053  raldifeq  4092  r19.3rz  4095  eldifpr  4237  eldiftp  4260  reusv2lem5  4903  prelpw  4944  otthg  4983  2rbropap  5046  rabxp  5188  elrng  5346  iss  5482  elimasni  5527  eliniseg  5529  xpcan  5605  xpcan2  5606  elpredg  5732  ordelpss  5789  fcnvres  6120  dffv3  6225  funimass4  6286  fndmdif  6361  fneqeql  6365  funimass3  6373  elrnrexdmb  6404  dff4  6413  fnsnb  6473  fconst4  6519  elunirn  6549  f12dfv  6569  riota1  6669  riota2df  6671  f1ocnvfv3  6686  eqfnov  6808  elrnmpt2res  6816  caoftrn  6974  ordsucun  7067  dflim3  7089  dfom2  7109  peano5  7131  opiota  7273  suppssr  7371  mpt2xopovel  7391  brtpos  7406  rntpos  7410  ordgt0ge1  7622  ondif2  7627  oelim2  7720  omabs  7772  iiner  7862  erinxp  7864  qliftfun  7875  mapdm0  7914  ordunifi  8251  elfi2  8361  elfiun  8377  fifo  8379  noinfep  8595  cantnflem1  8624  cantnf  8628  rankonidlem  8729  r1pwALT  8747  pr2nelem  8865  cardalephex  8951  alephinit  8956  dfac5lem4  8987  cflim2  9123  cfsmolem  9130  compssiso  9234  fin1a2lem11  9270  itunisuc  9279  axdclem  9379  brdom6disj  9392  alephreg  9442  fpwwe2lem9  9498  pwfseqlem3  9520  pwfseqlem4  9522  indpi  9767  nqereu  9789  ordpinq  9803  ltanq  9831  ltmnq  9832  suplem2pr  9913  map2psrpr  9969  ssxr  10145  letri3  10161  leltne  10165  ltneg  10566  leneg  10569  suprnub  11026  negiso  11041  elnnnn0  11374  nn0sub  11381  zrevaddcl  11460  znnsub  11461  znn0sub  11462  prime  11496  eluz2  11731  indstr  11794  eluz2b1  11797  qrevaddcl  11848  rpneg  11901  xrleltne  12016  dfle2  12018  dflt2  12019  xrletri3  12023  supxrleub  12194  infxrgelb  12203  ixxin  12230  iccid  12258  elicopnf  12307  iccsplit  12343  fzsplit2  12404  fzsn  12421  fzpr  12434  uzsplit  12450  preduz  12500  fvinim0ffz  12627  injresinj  12629  om2uzf1oi  12792  lt2sqi  12992  le2sqi  12993  hashsdom  13208  hashf1lem1  13277  fz1isolem  13283  prprrab  13293  ccatlcan  13518  ccatrcan  13519  s3eq3seq  13730  2swrd2eqwrdeq  13742  trclfvcotr  13794  cnpart  14024  limsuplt  14254  rlimresb  14340  mertenslem2  14661  fprod2dlem  14754  sadadd2lem2  15219  saddisjlem  15233  bitsuz  15243  gcddiv  15315  algcvgblem  15337  isprm3  15443  isprm5  15466  prmreclem5  15671  vdwapun  15725  vdwmc2  15730  ramcl  15780  pwsle  16199  ismre  16297  mreacs  16366  acsfn  16367  iscatd2  16389  cidpropd  16417  dfiso2  16479  oppcsect2  16486  isfunc  16571  setcinv  16787  lubeldm  17028  lubval  17031  glbeldm  17041  glbval  17044  tosso  17083  ipodrsfi  17210  acsfiindd  17224  imasmnd2  17374  submacs  17412  imasgrp2  17577  issubg  17641  resgrpisgrp  17662  subgacs  17676  eqgval  17690  gaorber  17787  symgfix2  17882  psgnran  17981  isslw  18069  sylow2alem2  18079  sylow2a  18080  sylow3lem6  18093  efgcpbllemb  18214  prmcyg  18341  gsum2d2lem  18418  gsumcom2  18420  subgdmdprd  18479  dprd2d2  18489  pgpfac1lem2  18520  pgpfac1lem4  18523  imasring  18665  drngmulne0  18817  lssle0  18998  lssacs  19015  lssats2  19048  lvecvsn0  19157  islpir  19297  isnzr2  19311  zndvds  19946  znleval  19951  znleval2  19952  lindsmm  20215  islinds3  20221  islindf4  20225  eltg2b  20811  discld  20941  opnssneib  20967  cldlp  21002  restbas  21010  leordtvallem1  21062  leordtvallem2  21063  ssidcn  21107  cnprest2  21142  lmss  21150  perfcls  21217  cmpfi  21259  1stccnp  21313  subislly  21332  hausmapdom  21351  locfindis  21381  iskgen3  21400  kgencn  21407  ptpjpre1  21422  xkoccn  21470  txrest  21482  txlm  21499  txkgen  21503  xkopt  21506  xkoinjcn  21538  imasnopn  21541  imasncld  21542  imasncls  21543  qtopcn  21565  kqfeq  21575  isr0  21588  fbfinnfr  21692  trfbas  21695  fbunfip  21720  ufileu  21770  cfinufil  21779  fmid  21811  txflf  21857  fclsrest  21875  alexsubALT  21902  tsmsres  21994  ucnima  22132  fmucndlem  22142  bldisj  22250  xmeter  22285  elbl4  22415  restmetu  22422  dscopn  22425  bl2ioo  22642  isphtpc  22840  tchcph  23082  lmmbr2  23103  lmmbrf  23106  iscau2  23121  iscauf  23124  caucfil  23127  metcld  23150  metcld2  23151  bcthlem1  23167  bcthlem4  23170  cldcss2  23259  ovolgelb  23294  ovoliunlem1  23316  ismbfcn  23443  mbfmax  23461  mbfimaopnlem  23467  i1faddlem  23505  i1fmullem  23506  i1fres  23517  i1fpos  23518  itg1climres  23526  xrge0f  23543  itgresr  23590  iblcnlem1  23599  limcun  23704  dvres  23720  mdegmullem  23883  ply1remlem  23967  plyremlem  24104  vieta1  24112  ulmcau  24194  sineq0  24318  coseq1  24319  ang180lem3  24586  cubic  24621  atandm  24648  atandm2  24649  atandm3  24650  rlimcnp  24737  rlimcnp2  24738  vmappw  24887  dchrelbas3  25008  dchrelbas4  25013  dchrsum2  25038  bposlem6  25059  dchrisumlem3  25225  pntleml  25345  istrkg3ld  25405  tgcgr4  25471  lnrot2  25564  islnopp  25676  islmib  25724  brbtwn2  25830  axsegconlem6  25847  axsegcon  25852  ax5seg  25863  axpasch  25866  axeuclid  25888  axcontlem4  25892  issubgr  26208  nb3gr2nb  26330  uhgrvd00  26486  isrusgr0  26518  wlkcpr  26580  wlkcomp  26582  upgr2wlk  26620  upgrf1istrl  26656  clwlkcomp  26731  iswwlksnx  26788  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  wspniunwspnon  26888  2pthon3v  26908  usgr2wspthons3  26931  usgr2wspthon  26932  rusgrnumwwlks  26941  clwlkclwwlklem3  26967  clwlkclwwlk  26968  clwwlknonelOLD  27071  0pth  27103  eupth2lem2  27197  vdgn1frgrv2  27276  fusgreg2wsp  27316  numclwwlkovgelOLD  27340  nmoolb  27754  nmlno0lem  27776  ubthlem1  27854  ocsh  28270  shle0  28429  eigrei  28821  adjeu  28876  nmoplb  28894  nmfnlb  28911  eleigvec2  28945  nmlnop0iALT  28982  cnlnadjlem5  29058  adjbdln  29070  jplem2  29256  cvbr2  29270  mdsl2bi  29310  chrelat3  29358  disjunsn  29533  ofpreima  29593  funcnvmpt  29596  funcnv5mpt  29597  dfcnv2  29604  gtiso  29606  fpwrelmap  29636  infxrge0glb  29658  xrdifh  29670  fzsplit3  29681  toslublem  29795  tosglblem  29797  isarchi  29864  xrge0tsmsbi  29914  smatrcl  29990  unitdivcld  30075  lmxrge0  30126  isrrext  30172  issibf  30523  eulerpartlemr  30564  eulerpartlemmf  30565  eulerpartlemn  30571  dstfrvunirn  30664  ballotlemfc0  30682  ballotlemfcc  30683  reprsuc  30821  reprpmtf1o  30832  reprdifc  30833  bnj919  30963  bnj976  30974  bnj1542  31053  bnj150  31072  bnj151  31073  bnj607  31112  bnj852  31117  bnj873  31120  bnj938  31133  bnj1171  31194  bnj1388  31227  bnj1489  31250  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem9  31307  kur14  31324  iscvm  31367  mclsax  31592  dfpo2  31771  elintfv  31788  fundmpss  31790  opelco3  31802  dfon2  31821  noetalem3  31990  dfbigcup2  32131  sscoid  32145  funpartfv  32177  dfrdg4  32183  cgr3permute3  32279  segletr  32346  segleantisym  32347  seglelin  32348  fneval  32472  neibastop3  32482  eltail  32494  filnetlem4  32501  bj-hbntbi  32820  bj-sbceqgALT  33022  bj-rest10  33166  bj-0int  33180  topdifinffinlem  33325  isbasisrelowllem1  33333  isbasisrelowllem2  33334  rdgeqoa  33348  finxpreclem4  33361  finxpsuclem  33364  uncf  33518  phpreu  33523  cos2h  33530  tan2h  33531  matunitlindflem1  33535  poimirlem16  33555  poimirlem19  33558  poimirlem23  33562  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  mbfposadd  33587  cnambfre  33588  itg2addnclem  33591  itg2addnc  33594  iblabsnclem  33603  ftc1anclem1  33615  ftc1anclem5  33619  caures  33686  heiborlem3  33742  heiborlem10  33749  elghomOLD  33816  divrngidl  33957  eqrelf  34161  brvbrvvdif  34169  eldmqsres2  34193  exanres  34204  ssrel3  34208  relcnveq  34234  iss2  34252  ecinn0  34258  brxrn2  34277  ecxrn  34289  eldmcoss2  34349  eldm1cossres  34350  elrelsrel  34377  elrelscnveq  34382  prtlem10  34469  prtlem16  34473  prtlem19  34482  prtex  34484  prter3  34486  islshpat  34622  lcvbr2  34627  lcvbr3  34628  lshpsmreu  34714  isat3  34912  hlrelat5N  35005  islpln5  35139  cdlemblem  35397  paddvaln0N  35405  paddval0  35414  cdlemefrs29bpre1  36002  cdlemefrs29cpre1  36003  cdlemg27b  36301  cdlemg33c  36313  cdlemg33e  36315  diaglbN  36661  cdlemm10N  36724  dicopelval2  36787  dicelval2N  36788  dihopelvalcpre  36854  dihglbcpreN  36906  dih1dimatlem  36935  dihatexv  36944  dvh4dimlem  37049  mapdpglem3  37281  hdmap14lem13  37489  hdmapglem7a  37536  isnacs2  37586  rabrenfdioph  37695  expdiophlem1  37905  pw2f1ocnv  37921  pwfi2f1o  37983  numinfctb  37990  dfacbasgrp  37995  islnr3  38002  subrgacs  38087  sdrgacs  38088  isdomn3  38099  dfhe3  38386  clsk3nimkb  38655  ntrneiiso  38706  ntrneikb  38709  hashnzfzclim  38838  dvconstbi  38850  sbc3orgOLD  39059  sbcel12gOLD  39071  rfcnpre3  39506  rfcnpre4  39507  unima  39660  cncfshift  40405  stoweidlem59  40594  nelbrnel  41617  iccpartiun  41695  oddm1evenALTV  41911  oddp1evenALTV  41912  oddprmne2  41949  submgmacs  42129  ismhm0  42130  iscmgmALT  42185  iscsgrpALT  42187  isrnghmmul  42218  elpglem2  42783
  Copyright terms: Public domain W3C validator