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

Theorem syl6ibr 240
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 216 . 2 (𝜒𝜃)
41, 3syl6 34 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3imtr4g  283  imp4aOLD  612  nic-ax  1588  nfimdOLD  2213  mo2v  2464  euim  2510  mopick2  2527  2moswap  2534  2eu6  2545  necon3d  2802  necon1d  2803  ralrimd  2941  spcimegf  3259  spcegf  3261  spcimedv  3264  spc2gv  3268  spc3gv  3270  rspcimedv  3283  eqsbc3rOLD  3459  tpid3gOLD  4248  pwpw0  4283  sssn  4295  pwsnALT  4361  ssiun  4492  ssiun2  4493  wefrc  5022  dmcosseq  5295  relssres  5344  restidsingOLD  5365  trin2  5425  ssrnres  5477  sossfld  5485  wfisg  5618  tron  5649  ordtri3or  5658  oneqmini  5679  fnun  5897  f1oun  6054  brprcneu  6081  ssimaex  6158  chfnrn  6221  dffo4  6268  dffo5  6269  tpres  6349  fvclss  6382  isomin  6465  isofrlem  6468  isoselem  6469  fnoprabg  6637  nnsuc  6951  f1oweALT  7020  bropopvvv  7119  bropfvvvvlem  7120  frxp  7151  poxp  7153  fnse  7158  mpt2xopynvov0g  7204  issmo2  7310  smores  7313  smogt  7328  rdglim2  7392  tz7.48lem  7400  tz7.49  7404  swoer  7636  qsss  7672  domtriord  7968  pssnn  8040  ssfi  8042  findcard  8061  findcard2  8062  findcard3  8065  frfi  8067  dffi3  8197  supmo  8218  infmo  8261  inf3lem4  8388  carddom2  8663  fidomtri2  8680  pm54.43  8686  infpwfien  8745  alephordi  8757  cardaleph  8772  carduniima  8779  cardinfima  8780  alephval3  8793  dfac5lem4  8809  dfac5  8811  dfac2  8813  kmlem2  8833  cflm  8932  cfslb2n  8950  cfsmolem  8952  isf32lem9  9043  axcc4  9121  domtriomlem  9124  zorn2lem4  9181  zorn2lem6  9183  fpwwe2lem11  9318  fpwwe2lem12  9319  inttsk  9452  inar1  9453  intgru  9492  ingru  9493  indpi  9585  nqpr  9692  ltaddpr  9712  ltexprlem1  9714  ltexprlem5  9718  reclem2pr  9726  reclem4pr  9728  negn0  10310  zmulcl  11259  uzm1  11550  uzwo  11583  xmullem2  11924  icoshft  12121  difreicc  12131  fzouzsplit  12327  ssfzoulel  12383  seqf1olem1  12657  seqf1olem2  12658  hashge2el2difr  13068  hashtpg  13071  swrdccatin2  13284  modfsummod  14313  incexclem  14353  sqrt2irr  14763  dvds2lem  14778  dvdslelem  14815  oddnn02np1  14856  divalglem8  14907  dfgcd2  15047  euclemma  15209  iserodd  15324  ramcl  15517  mreiincl  16025  joinfval  16770  meetfval  16784  dirge  17006  sylow2alem1  17801  efgredlemb  17928  kerf1hrm  18512  lbspss  18849  lspsneu  18890  lspsnat  18912  lspsncv0  18913  opsrtoslem2  19252  distop  20552  epttop  20565  isclo2  20644  restdis  20734  subbascn  20810  cnrest2  20842  cnpresti  20844  isnrm2  20914  cmpsublem  20954  cmpcld  20957  dfcon2  20974  t1conperf  20991  1stcrest  21008  lly1stc  21051  uptx  21180  txcn  21181  prdstopn  21183  txcon  21244  cmphaushmeo  21355  fbasrn  21440  csdfil  21450  trufil  21466  fclscf  21581  alexsubALTlem3  21605  alexsubALT  21607  haustsms2  21692  ovoliunlem1  22994  ovoliunnul  22999  volsup2  23096  coeaddlem  23726  plymul0or  23757  radcnv0  23891  wilthlem3  24513  chtub  24654  gausslemma2dlem1a  24807  2sqlem10  24870  pntpbnd1  24992  mptelee  25493  axeuclidlem  25560  axcontlem4  25565  usgrarnedg  25679  usgraedg4  25682  frgrancvvdeqlemA  26330  frgrancvvdeqlemC  26332  isch3  27288  shmodsi  27438  orthin  27495  h1datomi  27630  stcltr2i  28324  atom1d  28402  sumdmdii  28464  cdj3lem1  28483  disjpreima  28585  lmxrge0  29132  dmvlsiga  29325  sibfof  29535  bnj600  30049  bnj1018  30092  bnj1173  30130  bnj1174  30131  erdszelem9  30241  cvmlift2lem1  30344  fundmpss  30716  tfisg  30766  frinsg  30792  poseq  30800  sltval2  30859  nodenselem7  30892  nofulllem5  30911  outsideofrflx  31210  nn0prpwlem  31293  ivthALT  31306  fnessref  31328  neibastop2lem  31331  tailfb  31348  bj-axtd  31557  bj-ssbequ1  31639  bj-nfdt0  31678  bj-2upleq  31989  bj-restn0  32020  icorempt2  32171  isbasisrelowllem2  32176  matunitlindflem1  32371  poimirlem3  32378  poimirlem4  32379  poimirlem29  32404  mblfinlem3  32414  itg2addnclem3  32429  cover2  32474  fdc  32507  nninfnub  32513  equivtotbnd  32543  prdstotbnd  32559  cntotbnd  32561  ablo4pnp  32645  isdrngo3  32724  crngohomfo  32771  intidl  32794  or32dd  32862  prtlem18  32976  prter2  32980  lsat0cv  33134  lfl1  33171  lkreqN  33271  atlrelat1  33422  pmaple  33861  pmapsub  33868  pclclN  33991  pclfinN  34000  osumcllem4N  34059  pexmidlem1N  34070  cdleme7ga  34349  lcfl7N  35604  ss2iundf  36766  brtrclfv2  36834  nzss  37334  3impexpbicom  37502  alrim3con13v  37560  tratrb  37563  onfrALTlem3  37576  onfrALTlem2  37578  onfrALTlem1  37580  trsspwALT2  37864  trsspwALT3  37865  2reu1  39632  lighneallem4b  39862  bgoldbwt  39997  bgoldbst  39998  sgoldbalt  40001  lswn0  40040  uhgrissubgr  40494  nbgrnself2  40580  wlkOnl1iedg  40868  pthdivtx  40930  1wlkiswwlksupgr2  41069  eucrct2eupth  41408  2zrngamgm  41724  fldivexpfllog2  42152
  Copyright terms: Public domain W3C validator