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

Theorem syl6ibr 242
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.)
Hypotheses
Ref Expression
syl6ibr.1 (𝜑 → (𝜓𝜒))
syl6ibr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6ibr (𝜑 → (𝜓𝜃))

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6ibr.2 . . 3 (𝜃𝜒)
32biimpri 218 . 2 (𝜒𝜃)
41, 3syl6 35 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:  3imtr4g  285  imp4aOLD  614  nic-ax  1595  nfimt  1818  nfimdOLD  2225  mo2v  2476  euim  2522  mopick2  2539  2moswap  2546  2eu6  2557  necon3d  2811  necon1d  2812  ralrimd  2955  spcimegf  3277  spcegf  3279  spcimedv  3282  spc2gv  3286  spc3gv  3288  rspcimedv  3301  eqsbc3rOLD  3480  tpid3gOLD  4283  pwpw0  4319  sssn  4333  pwsnALT  4404  ssiun  4535  ssiun2  4536  wefrc  5078  ssrel  5178  dmcosseq  5357  relssres  5406  restidsingOLD  5428  trin2  5488  ssrnres  5541  sossfld  5549  wfisg  5684  tron  5715  ordtri3or  5724  oneqmini  5745  fnun  5965  f1oun  6123  brprcneu  6151  ssimaex  6230  chfnrn  6294  dffo4  6341  dffo5  6342  tpres  6431  fvclss  6465  isomin  6552  isofrlem  6555  isoselem  6556  fnoprabg  6726  nnsuc  7044  f1oweALT  7112  bropopvvv  7215  bropfvvvvlem  7216  frxp  7247  poxp  7249  fnse  7254  mpt2xopynvov0g  7300  issmo2  7406  smores  7409  smogt  7424  rdglim2  7488  tz7.48lem  7496  tz7.49  7500  swoer  7732  qsss  7768  domtriord  8066  pssnn  8138  ssfi  8140  findcard  8159  findcard2  8160  findcard3  8163  frfi  8165  dffi3  8297  supmo  8318  infmo  8361  inf3lem4  8488  carddom2  8763  fidomtri2  8780  pm54.43  8786  infpwfien  8845  alephordi  8857  cardaleph  8872  carduniima  8879  cardinfima  8880  alephval3  8893  dfac5lem4  8909  dfac5  8911  dfac2  8913  kmlem2  8933  cflm  9032  cfslb2n  9050  cfsmolem  9052  isf32lem9  9143  axcc4  9221  domtriomlem  9224  zorn2lem4  9281  zorn2lem6  9283  fpwwe2lem11  9422  fpwwe2lem12  9423  inttsk  9556  inar1  9557  intgru  9596  ingru  9597  indpi  9689  nqpr  9796  ltaddpr  9816  ltexprlem1  9818  ltexprlem5  9822  reclem2pr  9830  reclem4pr  9832  negn0  10419  zmulcl  11386  uzm1  11678  uzwo  11711  xmullem2  12054  icoshft  12252  difreicc  12262  fzouzsplit  12460  ssfzoulel  12519  seqf1olem1  12796  seqf1olem2  12797  hashge2el2difr  13217  hashtpg  13221  swrdccatin2  13440  modfsummod  14472  incexclem  14512  sqrt2irr  14922  dvds2lem  14937  dvdslelem  14974  oddnn02np1  15015  divalglem8  15066  dfgcd2  15206  euclemma  15368  iserodd  15483  ramcl  15676  setsstruct  15838  mreiincl  16196  joinfval  16941  meetfval  16955  dirge  17177  sylow2alem1  17972  efgredlemb  18099  kerf1hrm  18683  rmodislmodlem  18870  lbspss  19022  lspsneu  19063  lspsnat  19085  lspsncv0  19086  opsrtoslem2  19425  distop  20739  epttop  20753  isclo2  20832  restdis  20922  subbascn  20998  cnrest2  21030  cnpresti  21032  isnrm2  21102  cmpsublem  21142  cmpcld  21145  dfconn2  21162  t1connperf  21179  1stcrest  21196  lly1stc  21239  uptx  21368  txcn  21369  prdstopn  21371  txconn  21432  cmphaushmeo  21543  fbasrn  21628  csdfil  21638  trufil  21654  fclscf  21769  alexsubALTlem3  21793  alexsubALT  21795  haustsms2  21880  ovoliunlem1  23210  ovoliunnul  23215  volsup2  23313  coeaddlem  23943  plymul0or  23974  radcnv0  24108  wilthlem3  24730  chtub  24871  gausslemma2dlem1a  25024  2sqlem10  25087  pntpbnd1  25209  mptelee  25709  axeuclidlem  25776  axcontlem4  25781  uhgrissubgr  26094  nbgrnself2  26180  wlkonl1iedg  26464  pthdivtx  26528  wlkiswwlksupgr2  26666  eucrct2eupth  27005  isch3  27986  shmodsi  28136  orthin  28193  h1datomi  28328  stcltr2i  29022  atom1d  29100  sumdmdii  29162  cdj3lem1  29181  disjpreima  29283  lmxrge0  29822  dmvlsiga  30015  sibfof  30225  bnj600  30750  bnj1018  30793  bnj1173  30831  bnj1174  30832  erdszelem9  30942  cvmlift2lem1  31045  fundmpss  31421  tfisg  31470  frinsg  31496  poseq  31504  sltval2  31563  nodenselem7  31603  outsideofrflx  31929  nn0prpwlem  32012  ivthALT  32025  fnessref  32047  neibastop2lem  32050  tailfb  32067  bj-axtd  32273  bj-ssbequ1  32339  bj-nfdt0  32380  bj-2upleq  32700  bj-restn0  32733  icorempt2  32870  isbasisrelowllem2  32875  wl-ax8clv2  33052  matunitlindflem1  33076  poimirlem3  33083  poimirlem4  33084  poimirlem29  33109  mblfinlem3  33119  itg2addnclem3  33134  cover2  33179  fdc  33212  nninfnub  33218  equivtotbnd  33248  prdstotbnd  33264  cntotbnd  33266  ablo4pnp  33350  isdrngo3  33429  crngohomfo  33476  intidl  33499  or32dd  33567  prtlem18  33681  prter2  33685  lsat0cv  33839  lfl1  33876  lkreqN  33976  atlrelat1  34127  pmaple  34566  pmapsub  34573  pclclN  34696  pclfinN  34705  osumcllem4N  34764  pexmidlem1N  34775  cdleme7ga  35054  lcfl7N  36309  ss2iundf  37471  brtrclfv2  37539  nzss  38037  3impexpbicom  38206  alrim3con13v  38264  tratrb  38267  onfrALTlem3  38280  onfrALTlem2  38282  onfrALTlem1  38284  trsspwALT2  38568  trsspwALT3  38569  2reu1  40520  lswn0  40708  lighneallem4b  40855  bgoldbwt  40990  bgoldbst  40991  sgoldbalt  40994  isupwlkg  41036  2zrngamgm  41257  fldivexpfllog2  41681
  Copyright terms: Public domain W3C validator